proposition: Lemma cofinality_small x: infinite_c x -> \cf x <=c x.
proof: Proof. move => icx; rewrite - (cofinality_card icx). apply: (cofinality_c_small (proj1 icx)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)