proposition: Lemma infinite_union2 x y z: infinite_c z -> cardinal x <c z -> cardinal y <c z -> nonempty (z -s (x \cup y)).
proof: Proof. move => h1 h2 h3. move: (csum2_pr6_inf2 h1 h2 h3) => h. apply /nonemptyP => h4; move: (sub_smaller (empty_setC h4)). by rewrite (card_card (proj1 h1)) => /(cltNge h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)