Merge pull request #24 from ejgallego/dvdn_fact

[div] Move dvdn_fact from prime to div.

2 files changed, 6 insertions, 6 deletions

diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index e858d54..8179f57 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -457,6 +457,12 @@ Qed.
 Lemma dvdn_exp k d m : 0 < k -> d %| m -> d %| (m ^ k).
 Proof. by case: k => // k _ d_dv_m; rewrite expnS dvdn_mulr. Qed.
 
+Lemma dvdn_fact m n : 0 < m <= n -> m %| n`!.
+Proof.
+case: m => //= m; elim: n => //= n IHn; rewrite ltnS leq_eqVlt.
+by case/predU1P=> [-> | /IHn]; [apply: dvdn_mulr | apply: dvdn_mull].
+Qed.
+
 Hint Resolve dvdn_add dvdn_sub dvdn_exp.
 
 Lemma eqn_mod_dvd d m n : n <= m -> (m == n %[mod d]) = (d %| m - n).
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index b346a93..6b9720b 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -590,12 +590,6 @@ Proof. by move=> p_pr; rewrite /pdiv primes_exp ?primes_prime. Qed.
 
 (* Primes are unbounded. *)
 
-Lemma dvdn_fact m n : 0 < m <= n -> m %| n`!.
-Proof.
-case: m => //= m; elim: n => //= n IHn; rewrite ltnS leq_eqVlt.
-by case/predU1P=> [-> | /IHn]; [apply: dvdn_mulr | apply: dvdn_mull].
-Qed.
-
 Lemma prime_above m : {p | m < p & prime p}.
 Proof.
 have /pdivP[p pr_p p_dv_m1]: 1 < m`! + 1 by rewrite addn1 ltnS fact_gt0.