proposition: Lemma factorial2: factorial \2c = \2c.
proof: Proof. rewrite - succ_one. rewrite (factorial_succ NS1) factorial1 succ_one cprod1l; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)