proposition: Theorem countable_sub E F: sub E F -> countable_set F -> countable_set E.
proof: Proof. move=> /sub_smaller h1 /countableP h; apply /countableP; exact:cleT h1 h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)