proposition: Lemma regular_cardinalP x: regular_cardinal x <-> infinite_c x /\ \cf x = x.
proof: Proof. by split; move => [pa pb]; split => //; rewrite -{2} pb; move: (cofinality_card pa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)