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