Let n be given.

Assume Hn: n ∈ ω.

We will prove inv_nat n ∈ R.

We prove the intermediate claim HnSNoS: n ∈ SNoS_ ω.

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

We prove the intermediate claim HnR: n ∈ real.

An exact proof term for the current goal is (SNoS_omega_real n HnSNoS).

An exact proof term for the current goal is (real_recip_SNo n HnR).

∎