proposition: Lemma quotient_of_factorials a b: natp a -> natp b -> b <=c a -> (factorial b) %|c (factorial a).
proof: Proof. move=> aN bN ab; rewrite -(cdiff_rpr ab). move: (NS_diff b aN). set (c := a -c b);rewrite csumC; move: c; apply: Nat_induction. by rewrite (Nsum0r bN); apply: cdivides_itself; apply: NS_factorial. move => n nN. rewrite (csum_nS _ nN) (factorial_succ (NS_sum bN nN)). apply: cdivides_trans2; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)