Let X be given.

Assume HX: atleastp ω X.

Assume HXfin: finite X.

Apply HXfin to the current goal.

Let n be given.

Assume H.

Apply H to the current goal.

Assume Hn: n ∈ ω.

Assume H1: equip X n.

We will prove False.

Apply Pigeonhole_not_atleastp_ordsucc n (omega_nat_p n Hn) to the current goal.

We will prove atleastp (ordsucc n) n.

Apply atleastp_tra (ordsucc n) X n to the current goal.

We will prove atleastp (ordsucc n) X.

Apply atleastp_tra (ordsucc n) ω X to the current goal.

Apply Subq_atleastp to the current goal.

We will prove ordsucc n ⊆ ω.

Let i be given.

Assume Hi: i ∈ ordsucc n.

Apply nat_p_omega to the current goal.

We will prove nat_p i.

An exact proof term for the current goal is nat_p_trans (ordsucc n) (nat_ordsucc n (omega_nat_p n Hn)) i Hi.

We will prove atleastp ω X.

An exact proof term for the current goal is HX.

We will prove atleastp X n.

Apply equip_atleastp to the current goal.

An exact proof term for the current goal is H1.

∎