Let n be given.

Assume Hn: n ∈ int.

We prove the intermediate claim L0i: 0 ∈ 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_0.

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

Apply and3I to the current goal.

An exact proof term for the current goal is Hn.

We will prove 0 ∈ int.

An exact proof term for the current goal is L0i.

We use 0 to witness the existential quantifier.

Apply andI to the current goal.

We will prove 0 ∈ int.

An exact proof term for the current goal is L0i.

We will prove n * 0 = 0.

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

∎