Apply add_nat_add_SNo with
1,
1,
λ x0 x1 . x0 = 2 leaving 3 subgoals.
Apply nat_p_omega with
1.
The subproof is completed by applying nat_1.
Apply nat_p_omega with
1.
The subproof is completed by applying nat_1.
The subproof is completed by applying add_nat_1_1_2.