proposition: Lemma countable_setU2 a b: countable_set a -> countable_set b -> countable_set (a \cup b).
proof: Proof. move => /countableP ca /countableP cb; apply/countableP. move: (csum_Mlele ca cb); rewrite (csum_inf1 CIS_aleph0). by apply: cleT; move: (csum2_pr6 a b); rewrite - csum2cl - csum2cr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)