proposition: Lemma cofinality_c_small x: cardinalp x -> (cofinality_c x) <=c x.
proof: Proof. move => cx. case: (equal_or_not x \0c) => x0. by rewrite x0 cofinality_c_of0; apply:(cleR CS0). case: (equal_or_not x \1c) => x1. by rewrite x1 cofinality_c_of1; apply cle_01. by case: (cofinality_c_rw (cge2 cx x0 x1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)