proposition: Lemma infinite_greater_countable E: infinite_set E -> exists F, sub F E /\ cardinal F = aleph0.
proof: Proof. move=> /infinite_greater_countable1. rewrite aleph0_pr1 => /eq_subset_cardP1/set_leP [F e /card_eqP /esym ef]. by exists F. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)