We will prove k + 0 = m + 0 → k = m.

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

Assume H1: k = m.

An exact proof term for the current goal is H1.

Let n be given.

Assume Hn: nat_p n.

Assume IHn: k + n = m + n → k = m.

We will prove k + ordsucc n = m + ordsucc n → k = m.

rewrite the current goal using add_nat_SR k n Hn (from left to right).

rewrite the current goal using add_nat_SR m n Hn (from left to right).

We will prove ordsucc (k + n) = ordsucc (m + n) → k = m.

Assume H1: ordsucc (k + n) = ordsucc (m + n).

We will prove k = m.

Apply IHn to the current goal.

We will prove k + n = m + n.

Apply ordsucc_inj to the current goal.

An exact proof term for the current goal is H1.