proposition: Lemma induction_on_prod n f (prod := fun n=> cprodb n f): natp n -> prod (csucc n) = (prod n) *c (f n).
proof: Proof. move=> nN; rewrite /prod (succ_of_nat nN); apply cprodA_setU1. apply:(Nat_decent nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)