proposition: Lemma setU2_finite x y: finite_set x -> finite_set y -> finite_set (x \cup y).
proof: Proof. move=> /NatP cxN /NatP cyN; apply /NatP. move:(csum2_pr6 x y); rewrite - csum2cl - csum2cr => ha. apply: (NS_le_nat ha (NS_sum cxN cyN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)