proposition: Lemma regular_cardinal_omega: regular_cardinal omega0.
proof: Proof. move: CIS_omega => ico; split => //. move: (cofinality_c_small (proj1 ico)) => [_ _ pa]. move: (omega_limit3 (cofinality_infinite ico)) => pb. by apply: extensionality. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)