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.
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.
An
exact proof term for the current goal is
mul_nat_1R n.
∎