Let m and n be given.
Assume H1: divides_int m n.
Apply H1 to the current goal.
Assume H.
Apply H to the current goal.
Assume Hm: m ∈ int.
Assume Hn: n ∈ 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 H2: m * k = n.
We prove the intermediate claim LmS: SNo m.
An exact proof term for the current goal is int_SNo m Hm.
We prove the intermediate claim LnS: SNo n.
An exact proof term for the current goal is int_SNo n Hn.
We prove the intermediate claim LkS: SNo k.
An exact proof term for the current goal is int_SNo k Hk.
Apply xm (m = 0) to the current goal.
Assume H3: m = 0.
We will prove n :/: m ∈ int.
rewrite the current goal using H3 (from left to right).
rewrite the current goal using div_SNo_0_denum n LnS (from left to right).
We will prove 0 ∈ int.
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 nat_0.
Assume H3: m ≠ 0.
We prove the intermediate claim L1: n :/: m = k.
Apply mul_SNo_nonzero_cancel m (n :/: m) k LmS H3 (SNo_div_SNo n m LnS LmS) LkS to the current goal.
We will prove m * (n :/: m) = m * k.
rewrite the current goal using mul_div_SNo_invR n m LnS LmS H3 (from left to right).
We will prove n = m * k.
Use symmetry.
An exact proof term for the current goal is H2.
We will prove n :/: m ∈ int.
rewrite the current goal using L1 (from left to right).
An exact proof term for the current goal is Hk.
∎