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 int_SNo_cases to the current goal.
Let m be given.
Assume Hm: m ∈ ω.
Apply quotient_remainder_nat n Hn m (omega_nat_p m Hm) 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 = add_nat (mul_nat 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.
We prove the intermediate claim L1: m = q * n + r.
Use transitivity with and mul_nat q n + r.
We will prove m = mul_nat q n + r.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is add_nat_add_SNo (mul_nat q n) (nat_p_omega (mul_nat q n) (mul_nat_p q LqN n LnN)) r (nat_p_omega r LrN).
We will prove mul_nat q n + r = q * n + r.
Use f_equal.
An exact proof term for the current goal is mul_nat_mul_SNo q Hq n Hn1.
We use q to witness the existential quantifier.
Apply andI to the current goal.
We will prove q ∈ int.
Apply Subq_omega_int to the current goal.
An exact proof term for the current goal is Hq.
We use r to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hr.
We will prove m = q * n + r.
An exact proof term for the current goal is L1.
Let m be given.
Assume Hm: m ∈ ω.
We will prove ∃q ∈ int, ∃r ∈ n, - m = q * n + r.
Apply quotient_remainder_nat n Hn m (omega_nat_p m Hm) 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 = add_nat (mul_nat 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 LqS: SNo q.
Apply nat_p_SNo to the current goal.
An exact proof term for the current goal is LqN.
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.
We prove the intermediate claim LrS: SNo r.
Apply nat_p_SNo to the current goal.
An exact proof term for the current goal is LrN.
We prove the intermediate claim LnS: SNo n.
Apply nat_p_SNo to the current goal.
An exact proof term for the current goal is LnN.
We prove the intermediate claim LqnS: SNo (q * n).
An exact proof term for the current goal is SNo_mul_SNo q n LqS LnS.
We prove the intermediate claim L2: m = q * n + r.
Use transitivity with and mul_nat q n + r.
We will prove m = mul_nat q n + r.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is add_nat_add_SNo (mul_nat q n) (nat_p_omega (mul_nat q n) (mul_nat_p q LqN n LnN)) r (nat_p_omega r LrN).
We will prove mul_nat q n + r = q * n + r.
Use f_equal.
An exact proof term for the current goal is mul_nat_mul_SNo q Hq n Hn1.
We prove the intermediate claim L3: 0 ≤ r.
Apply omega_nonneg to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is LrN.
Apply SNoLeE 0 r SNo_0 LrS L3 to the current goal.
Assume H2: 0 < r.
We prove the intermediate claim L4: n + - r ∈ n.
Apply ordinal_SNoLt_In to the current goal.
We will prove ordinal (n + - r).
Apply nat_p_ordinal to the current goal.
We will prove nat_p (n + - r).
Apply nonneg_int_nat_p to the current goal.
We will prove n + - r ∈ int.
Apply int_add_SNo to the current goal.
Apply Subq_omega_int to the current goal.
An exact proof term for the current goal is Hn1.
Apply int_minus_SNo to the current goal.
Apply Subq_omega_int to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is LrN.
We will prove 0 ≤ n + - r.
Apply add_SNo_minus_Le2b n r 0 LnS LrS SNo_0 to the current goal.
We will prove 0 + r ≤ n.
rewrite the current goal using add_SNo_0L r LrS (from left to right).
Apply SNoLtLe to the current goal.
We will prove r < n.
An exact proof term for the current goal is ordinal_In_SNoLt n Lno r Hr.
We will prove ordinal n.
An exact proof term for the current goal is Lno.
We will prove n + - r < n.
Apply add_SNo_minus_Lt1b n r n LnS LrS LnS to the current goal.
We will prove n < n + r.
rewrite the current goal using add_SNo_0R n LnS (from right to left) at position 1.
We will prove n + 0 < n + r.
An exact proof term for the current goal is add_SNo_Lt2 n 0 r LnS SNo_0 LrS H2.
We use (- q + - 1) to witness the existential quantifier.
Apply andI to the current goal.
Apply int_add_SNo to the current goal.
Apply int_minus_SNo_omega to the current goal.
An exact proof term for the current goal is Hq.
Apply int_minus_SNo_omega to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_1.
We use (n + - r) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is L4.
We will prove - m = (- q + - 1) * n + (n + - r).
rewrite the current goal using mul_SNo_distrR (- q) (- 1) n (SNo_minus_SNo q LqS) (SNo_minus_SNo 1 SNo_1) LnS (from left to right).
We will prove - m = ((- q) * n + (- 1) * n) + (n + - r).
rewrite the current goal using mul_SNo_minus_distrL 1 n SNo_1 LnS (from left to right).
rewrite the current goal using mul_SNo_minus_distrL q n LqS LnS (from left to right).
We will prove - m = (- q * n + - 1 * n) + (n + - r).
rewrite the current goal using mul_SNo_oneL n LnS (from left to right).
We will prove - m = (- q * n + - n) + (n + - r).
rewrite the current goal using add_SNo_assoc (- q * n) (- n) (n + - r) (SNo_minus_SNo (q * n) LqnS) (SNo_minus_SNo n LnS) (SNo_add_SNo n (- r) LnS (SNo_minus_SNo r LrS)) (from right to left).
We will prove - m = - q * n + - n + n + - r.
rewrite the current goal using add_SNo_minus_L2 n (- r) LnS (SNo_minus_SNo r LrS) (from left to right).
We will prove - m = - q * n + - r.
rewrite the current goal using minus_add_SNo_distr (q * n) r LqnS LrS (from right to left).
Use f_equal.
An exact proof term for the current goal is L2.
Assume H2: 0 = r.
We use (- q) to witness the existential quantifier.
Apply andI to the current goal.
We will prove - q ∈ int.
Apply int_minus_SNo_omega 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 - m = (- q) * n + 0.
rewrite the current goal using mul_SNo_minus_distrL q n LqS LnS (from left to right).
We will prove - m = - (q * n) + 0.
rewrite the current goal using L2 (from left to right).
We will prove - (q * n + r) = - (q * n) + 0.
rewrite the current goal using H2 (from right to left).
We will prove - (q * n + 0) = - (q * n) + 0.
rewrite the current goal using add_SNo_0R (q * n) LqnS (from left to right).
Use symmetry.
An exact proof term for the current goal is add_SNo_0R (- q * n) (SNo_minus_SNo (q * n) LqnS).
∎