Let n be given.
Assume Hn.
Apply setminusE ω {0} n Hn to the current goal.
Assume Hn1: n ∈ ω.
Assume Hn2: n ∉ {0}.
We prove the intermediate claim LnN: nat_p n.
Apply omega_nat_p to the current goal.
An exact proof term for the current goal is Hn1.
We prove the intermediate claim Lno: ordinal n.
Apply nat_p_ordinal to the current goal.
An exact proof term for the current goal is LnN.
We prove the intermediate claim L0n: 0 ∈ n.
Apply ordinal_In_Or_Subq 0 n ordinal_Empty Lno to the current goal.
Assume H1: 0 ∈ n.
An exact proof term for the current goal is H1.
Assume H1: n ⊆ 0.
We will prove False.
Apply Hn2 to the current goal.
We will prove n ∈ {0}.
rewrite the current goal using Empty_Subq_eq n H1 (from left to right).
Apply SingI to the current goal.
Apply nat_ind to the current goal.
We will prove ∃q ∈ ω, ∃r ∈ n, 0 = q * n + r.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_0.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is L0n.
We will prove 0 = 0 * n + 0.
rewrite the current goal using mul_nat_0L n LnN (from left to right).
Use symmetry.
An exact proof term for the current goal is add_nat_0R 0.
Let m be given.
Assume Hm.
Assume IHm: ∃q ∈ ω, ∃r ∈ n, m = q * n + r.
We will prove ∃q ∈ ω, ∃r ∈ n, ordsucc m = q * n + r.
Apply IHm to the current goal.
Let q be given.
Assume H.
Apply H to the current goal.
Assume Hq: q ∈ ω.
Assume H.
Apply H to the current goal.
Let r be given.
Assume H.
Apply H to the current goal.
Assume Hr: r ∈ n.
Assume H1: m = q * n + r.
We prove the intermediate claim LqN: nat_p q.
An exact proof term for the current goal is omega_nat_p q Hq.
We prove the intermediate claim LrN: nat_p r.
An exact proof term for the current goal is nat_p_trans n LnN r Hr.
Apply ordinal_trichotomy_or_impred (ordsucc r) n (ordinal_ordsucc r (nat_p_ordinal r LrN)) Lno to the current goal.
Assume H2: ordsucc r ∈ n.
We use q to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hq.
We use (ordsucc r) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H2.
We will prove ordsucc m = q * n + ordsucc r.
rewrite the current goal using add_nat_SR (q * n) r LrN (from left to right).
Use f_equal.
An exact proof term for the current goal is H1.
Assume H2: ordsucc r = n.
We use (ordsucc q) to witness the existential quantifier.
Apply andI to the current goal.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is Hq.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is L0n.
We will prove ordsucc m = ordsucc q * n + 0.
rewrite the current goal using add_nat_0R (ordsucc q * n) (from left to right).
We will prove ordsucc m = ordsucc q * n.
rewrite the current goal using mul_nat_SL q LqN n LnN (from left to right).
We will prove ordsucc m = q * n + n.
rewrite the current goal using H2 (from right to left) at position 2.
We will prove ordsucc m = q * n + ordsucc r.
rewrite the current goal using add_nat_SR (q * n) r LrN (from left to right).
Use f_equal.
An exact proof term for the current goal is H1.
Assume H2: n ∈ ordsucc r.
We will prove False.
Apply In_irref n to the current goal.
Apply ordinal_ordsucc_In_Subq n Lno r Hr to the current goal.
An exact proof term for the current goal is H2.
∎