proposition: Lemma factorial_induction n: natp n -> factorial n = induction_term (fun a b => b *c(csucc a)) \1c n.
proof: Proof. move: n;apply: Nat_induction. by rewrite factorial0 induction_term0. by move=> m mN h; rewrite (factorial_succ mN) (induction_terms _ _ mN) h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)