Let n be given.

Assume Hn.

Let m be given.

Assume Hm.

rewrite the current goal using add_nat_add_SNo n Hn m Hm (from right to left).

Apply nat_p_omega to the current goal.

Apply add_nat_p to the current goal.

Apply omega_nat_p to the current goal.

An exact proof term for the current goal is Hn.

Apply omega_nat_p to the current goal.

An exact proof term for the current goal is Hm.

∎