proposition: Lemma infinite_greater_countable1 E: infinite_set E -> aleph0 <=c (cardinal E).
proof: Proof. move=>iE; have cE :=(CS_cardinal E). by split; [ exact CS_aleph0 | | apply/(omega_P1 (proj1 cE)) ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)