We will prove nat_p (n + 0).

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

We will prove nat_p n.

An exact proof term for the current goal is Hn.

Let m be given.

Assume Hm: nat_p m.

Assume IHm: nat_p (n + m).

We will prove nat_p (n + ordsucc m).

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

We will prove nat_p (ordsucc (n + m)).

Apply nat_ordsucc to the current goal.

We will prove nat_p (n + m).

An exact proof term for the current goal is IHm.