proposition: Lemma card_dominant_pr2: card_dominant omega0.
proof: Proof. have io: infinite_c omega0 by rewrite - aleph0E; apply: CIS_aleph; fprops. split => //. have lo: forall c, c <c omega0 <-> natp c. move=> c; split => h. by apply /olt_omegaP; apply: oclt. by apply: clt_fin_inf => //; apply /NatP. move=> a b /lo aN /lo bN; apply/lo; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)