proposition: Lemma dvdn_fact m n : 0 < m <= n -> m %| n`!.
proof: Proof. case: m => //= m; elim: n => //= n IHn; rewrite ltnS leq_eqVlt. by case/orP=> [/eqP-> | /IHn]; [apply: dvdn_mulr | apply: dvdn_mull]. Qed.
imports: mathcomp(all_ssreflect)