proposition: Lemma finite_union_finite f: (allf f finite_set) -> finite_set (domain f) -> finite_set (unionb f).
proof: Proof. move=> alf fsd. set (g:= Lg (domain f) (fun a => cardinal (Vg f a))). have dg: domain g = domain f by rewrite /g; aw. have fif: finite_int_fam g. hnf; rewrite /allf dg /g; split => //i idf. by rewrite LgV //;apply /NatP; apply: alf. move: (csum_pr1 f) (finite_sum_finite fif) => f2 xN. by apply/card_finite_setP; apply: (NS_le_nat f2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)