Let n be given.

Assume Hn.

Assume IH: ∀m, nat_p m → n ⊆ m → ∃k, nat_p k ∧ m = k + n.

Apply nat_inv_impred to the current goal.

Assume Hnm: ordsucc n ⊆ 0.

We will prove False.

Apply EmptyE n to the current goal.

We will prove n ∈ 0.

Apply Hnm to the current goal.

Apply ordsuccI2 to the current goal.

Let m be given.

Assume Hm: nat_p m.

Assume Hnm: ordsucc n ⊆ ordsucc m.

We prove the intermediate claim Lnm: n ⊆ m.

Apply ordinal_In_Or_Subq m n (nat_p_ordinal m Hm) (nat_p_ordinal n Hn) to the current goal.

Assume H1: m ∈ n.

We will prove False.

Apply In_irref (ordsucc m) to the current goal.

Apply Hnm to the current goal.

We will prove ordsucc m ∈ ordsucc n.

An exact proof term for the current goal is nat_ordsucc_in_ordsucc n Hn m H1.

Assume H1: n ⊆ m.

An exact proof term for the current goal is H1.

Apply IH m Hm Lnm to the current goal.

Let k be given.

Assume H.

Apply H to the current goal.

Assume Hk: nat_p k.

Assume H1: m = k + n.

We will prove ∃k, nat_p k ∧ ordsucc m = k + ordsucc n.

We use k to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hk.

We will prove ordsucc m = k + ordsucc n.

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

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

Use f_equal.

An exact proof term for the current goal is H1.