Let m and n be given.
Assume H1: divides_nat m n.
Apply H1 to the current goal.
Assume H.
Apply H to the current goal.
Assume Hm: m ∈ ω.
Assume Hn: n ∈ ω.
Assume H.
Apply H to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume Hk: k ∈ ω.
Assume H2: mul_nat m k = n.
We will prove m ∈ int ∧ n ∈ int ∧ ∃k ∈ int, m * k = n.
Apply and3I to the current goal.
Apply Subq_omega_int to the current goal.
An exact proof term for the current goal is Hm.
Apply Subq_omega_int 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 Subq_omega_int 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_nat_mul_SNo m Hm k Hk (from right to left).
We will prove mul_nat m k = n.
An exact proof term for the current goal is H2.
∎