proposition: Lemma factorial_prop f: f \0c = \1c -> (forall n, natp n -> f (csucc n) = (f n) *c (csucc n)) -> forall x, natp x -> f x = factorial x.
proof: Proof. move=> fz fp; apply: Nat_induction; first by rewrite factorial0. move=> m mN u; rewrite (factorial_succ mN) (fp _ mN) u // . Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)