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