proposition: Lemma dvdn_fact m n : 0 < m <= n -> m %| n`!.
proof: Proof. case: m => //= m; elim: n => //= n IHn; rewrite ltnS. have [/IHn/dvdn_mull->||-> _] // := ltngtP m n; exact: dvdn_mulr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)