Let X and Y be given.

Assume HcountY HsubXY.

We will prove atleastp X ω.

Apply atleastp_tra X Y ω to the current goal.

An exact proof term for the current goal is (Subq_atleastp X Y HsubXY).

An exact proof term for the current goal is HcountY.

∎