proposition: Lemma omega0_pr: [/\ ordinalp omega0, infinite_o omega0 & (forall z, ordinalp z -> infinite_o z -> sub omega0 z)].
proof: Proof. have p1: ordinalp (cardinal nat). by move: (CS_cardinal nat) => [ok _]. by move: (least_ordinal1 p1 nat_infinite_set). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)