Let n be given.
Assume Hn: nat_p n.
Let m be given.
Assume Hm: nat_p m.
Apply nat_ind to the current goal.
We will prove (n + m) + 0 = n + (m + 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 k be given.
Assume Hk: nat_p k.
Assume IHk: (n + m) + k = n + (m + k).
We will prove (n + m) + ordsucc k = n + (m + ordsucc k).
rewrite the current goal using (add_nat_SR (n + m) k Hk) (from left to right).
rewrite the current goal using (add_nat_SR m k Hk) (from left to right).
We will prove ordsucc ((n + m) + k) = n + ordsucc (m + k).
rewrite the current goal using add_nat_SR (from left to right).
We will prove ordsucc ((n + m) + k) = ordsucc (n + (m + k)).
rewrite the current goal using IHk (from left to right).
Use reflexivity.
We will prove nat_p (m + k).
An exact proof term for the current goal is add_nat_p m Hm k Hk.
∎