Let m be given.
Assume Hm.
Apply setminusE ω {0} m Hm to the current goal.
Assume Hm1: m ∈ ω.
Assume Hm2: m ∉ {0}.
We prove the intermediate claim LmN: nat_p m.
Apply omega_nat_p to the current goal.
An exact proof term for the current goal is Hm1.
We prove the intermediate claim Lmo: ordinal m.
Apply nat_p_ordinal to the current goal.
An exact proof term for the current goal is LmN.
We prove the intermediate claim LmZ: m ∈ int.
Apply Subq_omega_int to the current goal.
An exact proof term for the current goal is Hm1.
We prove the intermediate claim LmS: SNo m.
An exact proof term for the current goal is int_SNo m LmZ.
We prove the intermediate claim Lmpos: 0 < m.
Apply SNoLeE 0 m SNo_0 LmS (omega_nonneg m Hm1) to the current goal.
Assume H1: 0 < m.
An exact proof term for the current goal is H1.
Assume H1: 0 = m.
We will prove False.
Apply Hm2 to the current goal.
We will prove m ∈ {0}.
rewrite the current goal using H1 (from right to left).
Apply SingI to the current goal.
We will prove divides_int m m ∧ divides_int m m ∧ ∀d', divides_int d' m → divides_int d' m → d' ≤ m.
Apply and3I to the current goal.
We will prove divides_int m m.
Apply divides_int_ref to the current goal.
We will prove m ∈ int.
An exact proof term for the current goal is LmZ.
We will prove divides_int m m.
Apply divides_int_ref to the current goal.
An exact proof term for the current goal is LmZ.
Let d' be given.
Assume H1: divides_int d' m.
Assume _.
We will prove d' ≤ m.
Apply H1 to the current goal.
Assume H.
Apply H to the current goal.
Assume Hd': d' ∈ int.
Assume Hm: m ∈ int.
Assume H.
Apply H to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume Hk: k ∈ int.
Assume Hd'km: d' * k = m.
We will prove d' ≤ m.
We prove the intermediate claim Ld'S: SNo d'.
Apply int_SNo to the current goal.
An exact proof term for the current goal is Hd'.
We prove the intermediate claim LkS: SNo k.
Apply int_SNo to the current goal.
An exact proof term for the current goal is Hk.
Apply SNoLtLe_or 0 d' SNo_0 Ld'S to the current goal.
Assume H1: 0 < d'.
Apply SNoLtLe_or k 0 LkS SNo_0 to the current goal.
Assume H2: k < 0.
We will prove False.
Apply SNoLt_irref m to the current goal.
We will prove m < m.
Apply SNoLt_tra m 0 m LmS SNo_0 LmS to the current goal.
We will prove m < 0.
rewrite the current goal using Hd'km (from right to left).
An exact proof term for the current goal is mul_SNo_pos_neg d' k Ld'S LkS H1 H2.
An exact proof term for the current goal is Lmpos.
Assume H2: 0 ≤ k.
We prove the intermediate claim LkN: nat_p k.
An exact proof term for the current goal is nonneg_int_nat_p k Hk H2.
We prove the intermediate claim Ld'N: nat_p d'.
Apply nonneg_int_nat_p d' Hd' to the current goal.
We will prove 0 ≤ d'.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is H1.
Apply mul_nat_0_or_Subq d' Ld'N k LkN to the current goal.
Assume H3: k = 0.
We will prove False.
Apply SNoLt_irref m to the current goal.
We will prove m < m.
rewrite the current goal using Hd'km (from right to left) at position 1.
rewrite the current goal using H3 (from left to right).
We will prove d' * 0 < m.
rewrite the current goal using mul_SNo_zeroR d' Ld'S (from left to right).
We will prove 0 < m.
An exact proof term for the current goal is Lmpos.
Assume H3: d' ⊆ mul_nat d' k.
We will prove d' ≤ m.
rewrite the current goal using Hd'km (from right to left).
rewrite the current goal using mul_nat_mul_SNo d' (nat_p_omega d' Ld'N) k (nat_p_omega k LkN) (from right to left).
We will prove d' ≤ mul_nat d' k.
Apply ordinal_Subq_SNoLe to the current goal.
We will prove ordinal d'.
Apply nat_p_ordinal to the current goal.
An exact proof term for the current goal is Ld'N.
We will prove ordinal (mul_nat d' k).
Apply nat_p_ordinal to the current goal.
Apply mul_nat_p to the current goal.
An exact proof term for the current goal is Ld'N.
An exact proof term for the current goal is LkN.
We will prove d' ⊆ mul_nat d' k.
An exact proof term for the current goal is H3.
Assume H1: d' ≤ 0.
Apply SNoLe_tra d' 0 m Ld'S SNo_0 LmS H1 to the current goal.
We will prove 0 ≤ m.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Lmpos.
∎