Let n be given.

Assume Hn.

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

We will prove add_nat n 1 = ordsucc n.

rewrite the current goal using add_nat_SR n 0 nat_0 (from left to right).

We will prove ordsucc (add_nat n 0) = ordsucc n.

rewrite the current goal using add_nat_0R (from left to right).

Use reflexivity.

∎