proposition: Lemma cofinality_infinite_cardinal x: infinite_c x -> infinite_c (\cf x).
proof: Proof. move=> ix; apply: (cofinality_infinite_limit (infinite_card_limit2 ix)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)