Let m and n be given.
Assume H1 H2.
Apply H1 to the current goal.
Assume H _.
Apply H to the current goal.
Assume HmZ: m ∈ int.
Assume HnZ: n ∈ int.
We prove the intermediate claim LnS: SNo n.
Apply int_SNo to the current goal.
An exact proof term for the current goal is HnZ.
We prove the intermediate claim L1: ∀m ∈ int, divides_int m n → m ≤ n.
Apply int_SNo_cases to the current goal.
Let m be given.
Assume Hm: m ∈ ω.
Assume H3: divides_int m n.
Apply H3 to the current goal.
Assume _.
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 H4: m * k = n.
We will prove m ≤ n.
We prove the intermediate claim LmS: SNo m.
Apply omega_SNo to the current goal.
An exact proof term for the current goal is Hm.
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.
We will prove m ≤ n.
rewrite the current goal using H4 (from right to left).
We will prove m ≤ m * k.
rewrite the current goal using mul_SNo_oneR m LmS (from right to left) at position 1.
We will prove m * 1 ≤ m * k.
We prove the intermediate claim L0m: 0 ≤ m.
Apply omega_nonneg to the current goal.
An exact proof term for the current goal is Hm.
Apply nonneg_mul_SNo_Le m 1 k LmS to the current goal.
We will prove 0 ≤ m.
An exact proof term for the current goal is L0m.
An exact proof term for the current goal is SNo_1.
We will prove SNo k.
An exact proof term for the current goal is LkS.
We will prove 1 ≤ k.
Apply SNoLtLe_or k 1 LkS SNo_1 to the current goal.
Assume H5: k < 1.
We will prove False.
We prove the intermediate claim Lk0: k ≤ 0.
Apply SNoLtLe_or 0 k SNo_0 LkS to the current goal.
Assume H6: 0 < k.
We will prove False.
We prove the intermediate claim LkN: nat_p k.
Apply nonneg_int_nat_p k Hk to the current goal.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is H6.
Apply SNoLt_irref k to the current goal.
We will prove k < k.
Apply SNoLtLe_tra k 1 k LkS SNo_1 LkS H5 to the current goal.
We will prove 1 ≤ k.
Apply ordinal_Subq_SNoLe 1 k (ordinal_ordsucc 0 ordinal_Empty) (nat_p_ordinal k LkN) to the current goal.
We will prove 1 ⊆ k.
Apply ordinal_ordsucc_In_Subq k (nat_p_ordinal k LkN) 0 to the current goal.
We will prove 0 ∈ k.
Apply ordinal_SNoLt_In 0 k ordinal_Empty (nat_p_ordinal k LkN) to the current goal.
We will prove 0 < k.
An exact proof term for the current goal is H6.
Assume H6: k ≤ 0.
An exact proof term for the current goal is H6.
We prove the intermediate claim Lmk0: m * k ≤ 0.
rewrite the current goal using mul_SNo_com m k LmS LkS (from left to right).
Apply mul_SNo_nonpos_nonneg k m LkS LmS to the current goal.
We will prove k ≤ 0.
An exact proof term for the current goal is Lk0.
We will prove 0 ≤ m.
An exact proof term for the current goal is L0m.
Apply SNoLt_irref n to the current goal.
We will prove n < n.
rewrite the current goal using H4 (from right to left) at position 1.
We will prove m * k < n.
An exact proof term for the current goal is SNoLeLt_tra (m * k) 0 n (SNo_mul_SNo m k LmS LkS) SNo_0 LnS Lmk0 H2.
Assume H5: 1 ≤ k.
An exact proof term for the current goal is H5.
Let m be given.
Assume Hm: m ∈ ω.
Assume H3: divides_int (- m) n.
We prove the intermediate claim LmS: SNo m.
Apply omega_SNo to the current goal.
An exact proof term for the current goal is Hm.
We will prove - m ≤ n.
Apply SNoLe_tra (- m) 0 n (SNo_minus_SNo m LmS) SNo_0 LnS to the current goal.
We will prove - m ≤ 0.
rewrite the current goal using minus_SNo_0 (from right to left).
Apply minus_SNo_Le_contra 0 m SNo_0 LmS to the current goal.
We will prove 0 ≤ m.
Apply omega_nonneg to the current goal.
An exact proof term for the current goal is Hm.
We will prove 0 ≤ n.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is L1 m HmZ H1.
∎