We will prove 3 ∈ rational.

We prove the intermediate claim H3nat: nat_p 3.

rewrite the current goal using ordsucc_2_eq_3 (from right to left).

An exact proof term for the current goal is (nat_ordsucc 2 nat_2).

We prove the intermediate claim H3omega: 3 ∈ ω.

An exact proof term for the current goal is (nat_p_omega 3 H3nat).

We prove the intermediate claim H3SNoS: 3 ∈ SNoS_ ω.

An exact proof term for the current goal is (omega_SNoS_omega 3 H3omega).

An exact proof term for the current goal is (Subq_SNoS_omega_rational 3 H3SNoS).

∎