Let n be given.
Assume Hn: nat_p n.
Apply nat_ind to the current goal.
We will prove ordsucc n + 0 = ordsucc (n + 0).
rewrite the current goal using add_nat_0R (from left to right).
rewrite the current goal using add_nat_0R (from left to right).
Use reflexivity.
Let m be given.
Assume Hm: nat_p m.
Assume IHm: ordsucc n + m = ordsucc (n + m).
We will prove ordsucc n + ordsucc m = ordsucc (n + ordsucc m).
rewrite the current goal using (add_nat_SR (ordsucc n) m Hm) (from left to right).
We will prove ordsucc (ordsucc n + m) = ordsucc (n + ordsucc m).
rewrite the current goal using (add_nat_SR n m Hm) (from left to right).
We will prove ordsucc (ordsucc n + m) = ordsucc (ordsucc (n + m)).
rewrite the current goal using IHm (from left to right).
Use reflexivity.
∎