proposition: Lemma NS_factorial n: natp n -> natp (factorial n).
proof: Proof. move: n;apply: Nat_induction; first by rewrite factorial0; fprops. move=> m mN u; rewrite (factorial_succ mN); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)