proposition: Lemma sub_infinite_countable x: infinite_set x -> exists y, [/\ infinite_set y, countable_set y & sub y x].
proof: Proof. move /infinite_setP / infinite_c_P2; rewrite -/Nat - cardinal_Nat. move /eq_subset_cardP1 /set_leP => [y yx /card_eqP cy]. have iy: infinite_set y. apply/infinite_setP; rewrite - cy; apply/infinite_setP; apply: infinite_Nat. by exists y; split => //; apply /aleph0_countable; rewrite - cy - aleph0_pr1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)