rewrite the current goal using add_nat_add_SNo 1 (nat_p_omega 1 nat_1) 1 (nat_p_omega 1 nat_1) (from right to left).

An exact proof term for the current goal is add_nat_1_1_2.

∎