proposition: Lemma csum2_pr6_inf1 a b X: infinite_c X -> cardinal a <=c X -> cardinal b <=c X -> cardinal (a \cup b) <=c X.
proof: Proof. move => pa pb pc. move: (csum_Mlele pb pc); rewrite (csum_inf1 pa) csum2cl csum2cr. move: (csum2_pr6 a b); apply:cleT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)