proposition: Lemma induction_prod1 f a b: domain f = a +s1 b -> (~ inc b a) -> cprod f = cprod (restr f a) *c (Vg f b).
proof: Proof. by move=> df nba; rewrite - (induction_prod0 _ nba) - df - cprod_gr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)