Let n be given.
Assume Hn: n ∈ int.
We will prove n ∈ int ∧ n ∈ int ∧ ∃k ∈ int, n * k = n.
Apply and3I to the current goal.
An exact proof term for the current goal is Hn.
An exact proof term for the current goal is Hn.
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
We will prove 1 ∈ int.
Apply Subq_omega_int to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_1.
We will prove n * 1 = n.
An exact proof term for the current goal is mul_SNo_oneR n (int_SNo n Hn).
∎