proposition: Lemma CS_omega: cardinalp omega0.
proof: Proof. move: omega0_pr => [qa qb qc]; split => // z oz eq; apply: (qc _ oz). by apply:(EqT (EqT (EqS eq) qb)); apply /(succ_inf_aux_ord qa oz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)