proposition: Lemma countableP E: countable_set E <-> (cardinal E) <=c aleph0.
proof: Proof. apply: (iff_trans (eq_subset_cardP E Nat)). rewrite aleph0_pr1; apply:cardinal_le_aux2P; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)