proposition: Lemma finite_U2 x y: finite_set x -> finite_set y -> finite_set (x\cup y).
proof: Proof. move=> /card_finite_setP ns1 /card_finite_setP ns2; apply/card_finite_setP. move: (csum2_pr6 x y); rewrite - csum2cl - csum2cr => h. exact:(NS_le_nat h (NS_sum ns1 ns2)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)