proposition: Lemma binom_bad n m: natp n -> natp m -> n <c m -> binom n m = \0c.
proof: Proof. move=> nN mN h; move: (factorial_nz mN) (factorial_nz (NS_diff m nN))=> sa sb. move: (binom_alt_pr nN mN). by rewrite (Y_false (cltNge h)) => /cprod2_eq0; case => //;case/cprod2_eq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)