Let m be given.
Assume Hm: nat_p m.
Let k be given.
Assume Hk: k ∈ m.
Apply nat_ind to the current goal.
We will prove k + 0 ∈ 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).
An exact proof term for the current goal is Hk.
Let n be given.
Assume Hn: nat_p n.
Assume IHn: k + n ∈ m + n.
We will prove k + ordsucc n ∈ m + ordsucc n.
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).
Apply ordinal_ordsucc_In (m + n) (nat_p_ordinal (m + n) (add_nat_p m Hm n Hn)) (k + n) to the current goal.
We will prove k + n ∈ m + n.
An exact proof term for the current goal is IHn.
∎