Let n be given.
Assume Hn: nat_p n.
Apply nat_ind to the current goal.
We will prove n + 0 = 0 + n.
rewrite the current goal using (add_nat_0L n Hn) (from left to right).
An exact proof term for the current goal is (add_nat_0R n).
Let m be given.
Assume Hm: nat_p m.
Assume IHm: n + m = m + n.
We will prove n + ordsucc m = ordsucc m + n.
rewrite the current goal using (add_nat_SL m Hm n Hn) (from left to right).
We will prove n + ordsucc m = ordsucc (m + n).
rewrite the current goal using IHm (from right to left).
We will prove n + ordsucc m = ordsucc (n + m).
An exact proof term for the current goal is (add_nat_SR n m Hm).
∎