Let n be given.
Assume Hn: n ∈ ω.
We prove the intermediate claim Ln1: nat_p n.
An exact proof term for the current goal is omega_nat_p n Hn.
We prove the intermediate claim Ln2: ordinal n.
An exact proof term for the current goal is nat_p_ordinal n Ln1.
We prove the intermediate claim Ln3: SNo n.
An exact proof term for the current goal is ordinal_SNo n Ln2.
We prove the intermediate claim L1: ∀m, nat_p m → add_nat n m = n + m.
Apply nat_ind to the current goal.
We will prove add_nat n 0 = n + 0.
rewrite the current goal using add_SNo_0R n Ln3 (from left to right).
We will prove add_nat n 0 = n.
An exact proof term for the current goal is add_nat_0R n.
Let m be given.
Assume Hm: nat_p m.
Assume IH: add_nat n m = n + m.
We will prove add_nat n (ordsucc m) = n + (ordsucc m).
rewrite the current goal using add_SNo_ordinal_SR n Ln2 m (nat_p_ordinal m Hm) (from left to right).
We will prove add_nat n (ordsucc m) = ordsucc (n + m).
rewrite the current goal using IH (from right to left).
We will prove add_nat n (ordsucc m) = ordsucc (add_nat n m).
An exact proof term for the current goal is add_nat_SR n m Hm.
Let m be given.
Assume Hm: m ∈ ω.
We will prove add_nat n m = n + m.
An exact proof term for the current goal is L1 m (omega_nat_p m Hm).
∎