Let m be given.
Assume Hm.
Let n be given.
Assume Hn.
We will prove m ∈ ω ∧ m * n ∈ ω ∧ ∃k ∈ ω, m * k = m * n.
Apply and3I to the current goal.
An exact proof term for the current goal is Hm.
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 Hm.
Apply omega_nat_p to the current goal.
An exact proof term for the current goal is Hn.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn.
Use reflexivity.
∎