Let k, m and n be given.
Assume H1: divides_nat k m.
Assume H2: divides_nat m n.
Apply H1 to the current goal.
Assume H.
Apply H to the current goal.
Assume H1a: k ∈ ω.
Assume H1b: m ∈ ω.
Assume H1c: ∃u ∈ ω, k * u = m.
Apply H1c to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Assume Hu: u ∈ ω.
Assume H1d: k * u = m.
Apply H2 to the current goal.
Assume H.
Apply H to the current goal.
Assume H2a: m ∈ ω.
Assume H2b: n ∈ ω.
Assume H2c: ∃v ∈ ω, m * v = n.
Apply H2c to the current goal.
Let v be given.
Assume H.
Apply H to the current goal.
Assume Hv: v ∈ ω.
Assume H2d: m * v = n.
We will prove k ∈ ω ∧ n ∈ ω ∧ ∃w ∈ ω, k * w = n.
Apply and3I to the current goal.
An exact proof term for the current goal is H1a.
An exact proof term for the current goal is H2b.
We use u * v to witness the existential quantifier.
Apply andI to the current goal.
We will prove u * v ∈ ω.
Apply nat_p_omega to the current goal.
Apply mul_nat_p to the current goal.
Apply omega_nat_p to the current goal.
An exact proof term for the current goal is Hu.
Apply omega_nat_p to the current goal.
An exact proof term for the current goal is Hv.
We will prove k * (u * v) = n.
rewrite the current goal using mul_nat_asso k (omega_nat_p k H1a) u (omega_nat_p u Hu) v (omega_nat_p v Hv) (from right to left).
We will prove (k * u) * v = n.
rewrite the current goal using H1d (from left to right).
We will prove m * v = n.
An exact proof term for the current goal is H2d.
∎