proposition: Lemma factorial_monotone a b: natp b -> a <=c b -> factorial a <=c factorial b.
proof: Proof. move => bN leab. move:(NS_le_nat leab bN) => aN. apply: (cdivides_smaller (quotient_of_factorials bN aN leab)). apply: (factorial_nz bN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)