Let m be given.

Assume Hm.

Let n be given.

Assume Hn.

We will prove m ∈ ω ∧ m * n ∈ ω ∧ ∃k ∈ ω, mul_nat m k = m * n.

Apply and3I to the current goal.

An exact proof term for the current goal is Hm.

Apply mul_SNo_In_omega 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 n to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hn.

We will prove mul_nat m n = m * n.

An exact proof term for the current goal is mul_nat_mul_SNo m Hm n Hn.

∎