proposition: Lemma quotient_of_factorials1 a b: natp a -> natp b -> b <=c a -> (factorial (a -c b)) %|c (factorial a).
proof: Proof. move=> aN bN leab; apply: (quotient_of_factorials aN); fprops. exact:cdiff_ab_le_a (proj32 leab). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)