proposition: Lemma cofinality_infinite_limit x: limit_ordinal x -> infinite_c (\cf x).
proof: Proof. move=> ix; split; first by apply: (CS_cofinality (proj31 ix)). apply: OIS_limit; apply: (cofinality_limit3 ix). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)