proposition: Lemma finite_is_countable X: finite_set X -> countable_set X.
proof: Proof. move => /card_finite_setP /NatP h; apply/countableP. apply(cle_fin_inf h CIS_aleph0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)