Let n be given.

Assume Hn: n ∈ int.

We will prove 1 ∈ int ∧ n ∈ int ∧ ∃k ∈ int, 1 * k = n.

Apply and3I to the current goal.

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.

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 1 * n = n.

An exact proof term for the current goal is mul_SNo_oneL n (int_SNo n Hn).

∎