We will prove 0 + 0 = 0.

Apply add_nat_0R to the current goal.

Let m be given.

Assume Hm: nat_p m.

Assume IHm: 0 + m = m.

We will prove 0 + ordsucc m = ordsucc m.

rewrite the current goal using (add_nat_SR 0 m Hm) (from left to right).

We will prove ordsucc (0 + m) = ordsucc m.

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

Use reflexivity.