We will prove infinite ω.

We prove the intermediate claim Hatleast: atleastp ω ω.

An exact proof term for the current goal is (Subq_atleastp ω ω (Subq_ref ω)).

An exact proof term for the current goal is (atleastp_omega_infinite ω Hatleast).

∎