proposition: Lemma factorial_nz n: natp n -> factorial n <> \0c.
proof: Proof. move: n;apply: Nat_induction. rewrite factorial0; exact: card1_nz. move=> m mN u; rewrite (factorial_succ mN). apply: cprod2_nz =>//; apply: succ_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)