proposition: Lemma factorial_succ n: natp n -> factorial (csucc n) = (factorial n) *c (csucc n).
proof: Proof. move=> nN; exact:(induction_on_prod csucc nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)