proposition: Lemma finite_product_finite_aux x: sub x (domain f) -> natp (cprod (restr f x)).
proof: Proof. move: fif => [alN fsd] sxd. have fsx:=(sub_finite_set sxd fsd). move: x fsx sxd; apply: finite_set_induction0. rewrite cprod_trivial;fprops; aww. move=> a b ap nba st; rewrite induction_prod0 =>//. apply:NS_prod;[apply: ap; apply: sub_trans st | ];fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)