proposition: Lemma ffact_gt0 n m : natp n -> m <=c n -> n ^_c m <> \0c.
proof: Proof. move => nN le; move: (NS_le_nat le nN) => mN. move: m mN n nN le; apply: Nat_induction. move => n _ _; rewrite ffactn0; fprops. move => m mN Hrec n nN le. case: (equal_or_not n \0c) => nz. by move: le; rewrite nz => /cle0 /succ_nz. move: (cpred_pr nN nz) => [sa sb]. rewrite (ffactnS nN mN); apply: cprod2_nz; first by rewrite sb; apply:succ_nz. by apply: (Hrec _ sa);apply/(cleSSP (CS_nat mN) (CS_nat sa)); rewrite - sb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)