Added and generalized arithmetic theorems. (#394)

- Added: `modn_divl` and `divn_modl`.
- Generalized `muln_modr` and `muln_modl` removing hypothesis `0 < p`.

2 files changed, 18 insertions, 3 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index c03b4f8..97ee41a 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -30,6 +30,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   `big_enum_val_cond`, `big_enum_rank_cond`,
   `big_enum_val`, `big_enum_rank`, `big_set`.
 
+- Arithmetic theorems: `modn_divl` and `divn_modl`.
+
 ### Changed
 
 - `eqVneq` lemma is changed from `{x = y} + {x != y}` to
@@ -41,6 +43,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - Generalized the `allpairs_catr` lemma to the case where the types of `s`,
   `t1`, and `t2` are non-`eqType`s in `[seq E | i <- s, j <- t1 ++ t2]`.
 
+- Generalized `muln_modr` and `muln_modl` removing hypothesis `0 < p`.
+
 ### Infrastructure
 
 - `Makefile` now supports the `test-suite` and `only` targets. Currently,
diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index 3cb98e8..d71db3a 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -220,15 +220,23 @@ case: (posnP d) => [-> | d_gt0]; first by rewrite muln0.
 by rewrite {1}(divn_eq m d) addnA -mulnDl modn_def edivn_eq // ltn_mod.
 Qed.
 
-Lemma muln_modr {p m d} : 0 < p -> p * (m %% d) = (p * m) %% (p * d).
+Lemma muln_modr p m d : p * (m %% d) = (p * m) %% (p * d).
 Proof.
-move=> p_gt0; apply: (@addnI (p * (m %/ d * d))).
+have [->//|p_gt0] := posnP p; apply: (@addnI (p * (m %/ d * d))).
 by rewrite -mulnDr -divn_eq mulnCA -(divnMl p_gt0) -divn_eq.
 Qed.
 
-Lemma muln_modl {p m d} : 0 < p -> (m %% d) * p = (m * p) %% (d * p).
+Lemma muln_modl p m d : (m %% d) * p = (m * p) %% (d * p).
 Proof. by rewrite -!(mulnC p); apply: muln_modr. Qed.
 
+Lemma modn_divl m n d : (m %/ d) %% n = m %% (n * d) %/ d.
+Proof.
+case: d n => [|d] [|n] //; rewrite [in LHS]/divn [in LHS]modn_def.
+case: (edivnP m d.+1) edivnP => [/= _ r -> le_rd] [/= q s -> le_sn].
+rewrite mulnDl -mulnA -addnA modnMDl modn_small ?divnMDl ?divn_small ?addn0//.
+by rewrite mulSnr -addnS leq_add ?leq_mul2r.
+Qed.
+
 Lemma modnDl m d : d + m = m %[mod d].
 Proof. by rewrite -{1}[d]mul1n modnMDl. Qed.
 
@@ -428,6 +436,9 @@ Qed.
 Lemma dvdn_exp2r m n k : m %| n -> m ^ k %| n ^ k.
 Proof. by case/dvdnP=> q ->; rewrite expnMn dvdn_mull. Qed.
 
+Lemma divn_modl m n d : d %| n -> (m %% n) %/ d = (m %/ d) %% (n %/ d).
+Proof. by move=> dvd_dn; rewrite modn_divl divnK. Qed.
+
 Lemma dvdn_addr m d n : d %| m -> (d %| m + n) = (d %| n).
 Proof. by case/dvdnP=> q ->; rewrite /dvdn modnMDl. Qed.