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 will prove m ∈ int ∧ - n ∈ int ∧ ∃k ∈ int, m * k = - n.
Apply and3I to the current goal.
An exact proof term for the current goal is Hm.
Apply int_minus_SNo to the current goal.
An exact proof term for the current goal is Hn.
We use - k to witness the existential quantifier.
Apply andI to the current goal.
Apply int_minus_SNo to the current goal.
An exact proof term for the current goal is Hk.
We will prove m * (- k) = - n.
rewrite the current goal using mul_SNo_minus_distrR m k (int_SNo m Hm) (int_SNo k Hk) (from left to right).
We will prove - m * k = - n.
Use f_equal.
An exact proof term for the current goal is H2.
∎