proposition: Lemma ffact_small n m : natp m -> n <c m -> n ^_c m = \0c.
proof: Proof. move => mN. move: m mN n; apply: Nat_induction; first by move=> n /clt0. move => m mN Hrec n lt. move:(NS_lt_nat lt (NS_succ mN)) => nN. rewrite (ffactnS nN mN). case: (equal_or_not n \0c) => nz; first by rewrite nz cprod0l. move: (cpred_pr nN nz) => [sa sb]. move: lt; rewrite {1} sb => /(cltSSP (CS_nat sa) (CS_nat mN)) /Hrec ->. by apply: cprod0r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)