Let n be given.
Assume Hn.
We prove the intermediate claim Ln: n ∈ ω.
An exact proof term for the current goal is nat_p_omega n Hn.
We will prove n ∈ ω ∧ n ∈ ω ∧ ∃k ∈ ω, n * k = n.
Apply and3I to the current goal.
An exact proof term for the current goal is Ln.
An exact proof term for the current goal is Ln.
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
We will prove 1 ∈ ω.
An exact proof term for the current goal is nat_p_omega 1 nat_1.
We will prove n * 1 = n.
An exact proof term for the current goal is mul_nat_1R n.
∎