proposition: Lemma finite_product_finite_set f: (allf f finite_set) -> finite_set (domain f) -> finite_set(productb 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. rewrite/finite_set -/(cprod _) cprod_pr; apply: Nat_hi. apply: finite_product_finite; split; last ue. by hnf; aw; move=> i idf; rewrite LgV //; apply /NatP;apply: alf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)