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