Merge pull request #607 from pi8027/distr-suffixes

Switch from long suffixes to short suffixes

9 files changed, 127 insertions, 81 deletions

diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index 4cf0cef..e8293ae 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -443,14 +443,21 @@ Lemma addmCA : left_commutative add. Proof. exact: mulmCA. Qed.
 Lemma addmAC : right_commutative add. Proof. exact: mulmAC. Qed.
 Lemma add0m : left_id idm add. Proof. exact: mul1m. Qed.
 Lemma addm0 : right_id idm add. Proof. exact: mulm1. Qed.
-Lemma mulm_addl : left_distributive mul add. Proof. by case add. Qed.
-Lemma mulm_addr : right_distributive mul add. Proof. by case add. Qed.
+Lemma mulmDl : left_distributive mul add. Proof. by case add. Qed.
+Lemma mulmDr : right_distributive mul add. Proof. by case add. Qed.
 End Add.
 
 Definition simpm := (mulm1, mulm0, mul1m, mul0m, mulmA).
 
 End Theory.
 
+Notation "@ 'mulm_addl'" :=
+  (deprecate mulm_addl mulmDl) (at level 10, only parsing) : fun_scope.
+Notation "@ 'mulm_addr'" :=
+  (deprecate mulm_addr mulmDr) (at level 10, only parsing) : fun_scope.
+Notation mulm_addl := (@mulm_addl _ _ _) (only parsing).
+Notation mulm_addr := (@mulm_addr _ _ _) (only parsing).
+
 End Theory.
 Include Theory.
 
@@ -483,7 +490,7 @@ Canonical addn_addoid := AddLaw mulnDl mulnDr.
 
 Canonical maxn_monoid := Law maxnA max0n maxn0.
 Canonical maxn_comoid := ComLaw maxnC.
-Canonical maxn_addoid := AddLaw maxn_mull maxn_mulr.
+Canonical maxn_addoid := AddLaw maxnMl maxnMr.
 
 Canonical gcdn_monoid := Law gcdnA gcd0n gcdn0.
 Canonical gcdn_comoid := ComLaw gcdnC.
@@ -954,7 +961,7 @@ Lemma big_addn m n a (P : pred nat) F :
   \big[op/idx]_(m + a <= i < n | P i) F i =
      \big[op/idx]_(m <= i < n - a | P (i + a)) F (i + a).
 Proof.
-rewrite /index_iota -subnDA addnC iota_addl big_map.
+rewrite /index_iota -subnDA addnC iotaDl big_map.
 by apply: eq_big => ? *; rewrite addnC.
 Qed.
 
@@ -1277,7 +1284,7 @@ Lemma big_cat_nat n m p (P : pred nat) F : m <= n -> n <= p ->
   \big[*%M/1]_(m <= i < p | P i) F i =
    (\big[*%M/1]_(m <= i < n | P i) F i) * (\big[*%M/1]_(n <= i < p | P i) F i).
 Proof.
-move=> le_mn le_np; rewrite -big_cat -{2}(subnKC le_mn) -iota_add subnDA.
+move=> le_mn le_np; rewrite -big_cat -{2}(subnKC le_mn) -iotaD subnDA.
 by rewrite subnKC // leq_sub.
 Qed.
 
@@ -1315,8 +1322,7 @@ Proof.
 rewrite -(big_map _ _ (lshift n) _ P F) -(big_map _ _ (@rshift m _) _ P F).
 rewrite -big_cat; congr bigop; apply: (inj_map val_inj).
 rewrite map_cat -!map_comp (map_comp (addn m)) /=.
-rewrite ![index_enum _]unlock unlock !val_ord_enum.
-by rewrite -iota_addl addn0 iota_add.
+by rewrite ![index_enum _]unlock unlock !val_ord_enum -iotaDl addn0 iotaD.
 Qed.
 
 Lemma big_flatten I rr (P : pred I) F :
@@ -1739,11 +1745,11 @@ Local Notation "x + y" := (plus x y).
 
 Lemma big_distrl I r a (P : pred I) F :
   \big[+%M/0]_(i <- r | P i) F i * a = \big[+%M/0]_(i <- r | P i) (F i * a).
-Proof. by rewrite (big_endo ( *%M^~ a)) ?mul0m // => x y; apply: mulm_addl. Qed.
+Proof. by rewrite (big_endo ( *%M^~ a)) ?mul0m // => x y; apply: mulmDl. Qed.
 
 Lemma big_distrr I r a (P : pred I) F :
   a * \big[+%M/0]_(i <- r | P i) F i = \big[+%M/0]_(i <- r | P i) (a * F i).
-Proof. by rewrite big_endo ?mulm0 // => x y; apply: mulm_addr. Qed.
+Proof. by rewrite big_endo ?mulm0 // => x y; apply: mulmDr. Qed.
 
 Lemma big_distrlr I J rI rJ (pI : pred I) (pJ : pred J) F G :
   (\big[+%M/0]_(i <- rI | pI i) F i) * (\big[+%M/0]_(j <- rJ | pJ j) G j)
diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index 17e3ac4..4899ee3 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -326,7 +326,7 @@ Proof. by rewrite [in RHS](divn_eq m 2) modn2 muln2 addnC half_bit_double. Qed.
 
 Lemma odd_mod m d : odd d = false -> odd (m %% d) = odd m.
 Proof.
-by move=> d_even; rewrite [in RHS](divn_eq m d) oddD odd_mul d_even andbF.
+by move=> d_even; rewrite [in RHS](divn_eq m d) oddD oddM d_even andbF.
 Qed.
 
 Lemma modnXm m n a : (a %% n) ^ m = a ^ m %[mod n].
@@ -937,33 +937,33 @@ Qed.
 Lemma Gauss_gcdl p m n : coprime p n -> gcdn p (m * n) = gcdn p m.
 Proof. by move=> co_pn; rewrite mulnC Gauss_gcdr. Qed.
 
-Lemma coprime_mulr p m n : coprime p (m * n) = coprime p m && coprime p n.
+Lemma coprimeMr p m n : coprime p (m * n) = coprime p m && coprime p n.
 Proof.
 case co_pm: (coprime p m) => /=; first by rewrite /coprime Gauss_gcdr.
 apply/eqP=> co_p_mn; case/eqnP: co_pm; apply gcdn_def => // d dv_dp dv_dm.
 by rewrite -co_p_mn dvdn_gcd dv_dp dvdn_mulr.
 Qed.
 
-Lemma coprime_mull p m n : coprime (m * n) p = coprime m p && coprime n p.
-Proof. by rewrite -!(coprime_sym p) coprime_mulr. Qed.
+Lemma coprimeMl p m n : coprime (m * n) p = coprime m p && coprime n p.
+Proof. by rewrite -!(coprime_sym p) coprimeMr. Qed.
 
 Lemma coprime_pexpl k m n : 0 < k -> coprime (m ^ k) n = coprime m n.
 Proof.
 case: k => // k _; elim: k => [|k IHk]; first by rewrite expn1.
-by rewrite expnS coprime_mull -IHk; case coprime.
+by rewrite expnS coprimeMl -IHk; case coprime.
 Qed.
 
 Lemma coprime_pexpr k m n : 0 < k -> coprime m (n ^ k) = coprime m n.
 Proof. by move=> k_gt0; rewrite !(coprime_sym m) coprime_pexpl. Qed.
 
-Lemma coprime_expl k m n : coprime m n -> coprime (m ^ k) n.
+Lemma coprimeXl k m n : coprime m n -> coprime (m ^ k) n.
 Proof. by case: k => [|k] co_pm; rewrite ?coprime1n // coprime_pexpl. Qed.
 
-Lemma coprime_expr k m n : coprime m n -> coprime m (n ^ k).
-Proof. by rewrite !(coprime_sym m); apply: coprime_expl. Qed.
+Lemma coprimeXr k m n : coprime m n -> coprime m (n ^ k).
+Proof. by rewrite !(coprime_sym m); apply: coprimeXl. Qed.
 
 Lemma coprime_dvdl m n p : m %| n -> coprime n p -> coprime m p.
-Proof. by case/dvdnP=> d ->; rewrite coprime_mull => /andP[]. Qed.
+Proof. by case/dvdnP=> d ->; rewrite coprimeMl => /andP[]. Qed.
 
 Lemma coprime_dvdr m n p : m %| n -> coprime p n -> coprime p m.
 Proof. by rewrite !(coprime_sym p); apply: coprime_dvdl. Qed.
@@ -1040,3 +1040,12 @@ by rewrite chinese_modl chinese_modr !modn_mod !eqxx.
 Qed.
 
 End Chinese.
+
+Notation "@ 'coprime_expl'" :=
+  (deprecate coprime_expl coprimeXl) (at level 10, only parsing) : fun_scope.
+Notation "@ 'coprime_expr'" :=
+  (deprecate coprime_expr coprimeXr) (at level 10, only parsing) : fun_scope.
+Notation coprime_mull := (deprecate coprime_mull coprimeMl) (only parsing).
+Notation coprime_mulr := (deprecate coprime_mulr coprimeMr) (only parsing).
+Notation coprime_expl := (fun k => @coprime_expl k _ _) (only parsing).
+Notation coprime_expr := (fun k => @coprime_expr k _ _) (only parsing).
diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index b77d1a8..5c933cf 100644
--- a/mathcomp/ssreflect/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
@@ -499,8 +499,8 @@ Lemma iter_finv_in n :
   {in S, forall x, n <= order x -> iter n finv x = iter (order x - n) f x}.
 Proof.
 move=> x xS; rewrite -[x in LHS]iter_order_in => // /subnKC {1}<-.
-move: (_ - n) => m; rewrite iter_add; elim: n => // n {2}<-.
-by rewrite iterSr /= finv_f_in // -iter_add iter_in.
+move: (_ - n) => m; rewrite iterD; elim: n => // n {2}<-.
+by rewrite iterSr /= finv_f_in // -iterD iter_in.
 Qed.
 
 Lemma cycle_orbit_in : {in S, forall x, (fcycle f) (orbit x)}.
@@ -810,8 +810,8 @@ tfae=> [xorbit_cycle|||[k fkx]|fx y z|/injectivePcycle//].
 - apply: (@iter_order_cycle (traject f x k.+1)); rewrite /= ?mem_head//.
   by apply/fpathP; exists k.+1; rewrite trajectSr -iterSr fkx.
 - rewrite -!fconnect_orbit => /iter_findex <- /iter_findex <-.
-  move=> /(congr1 (iter (order x).-1 f)); rewrite  -!iterSr !orderSpred.
-  by rewrite -!iter_add ![order _ + _]addnC !iter_add fx.
+  move/(congr1 (iter (order x).-1 f)).
+  by rewrite -!iterSr !orderSpred -!iterD ![order _ + _]addnC !iterD fx.
 Qed.
 
 Lemma order_id_cycle x : fcycle f (orbit x) -> order (f x) = order x.
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 4a3eaf1..5b6e4d0 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -2289,7 +2289,7 @@ Definition fixset := iterF n.
 Lemma fixsetK : F fixset = fixset.
 Proof.
 suff /'exists_eqP[x /= e]: [exists k : 'I_n.+1, iterF k == iterF k.+1].
-  by rewrite /fixset -(subnK (leq_ord x)) /iterF iter_add iter_fix.
+  by rewrite /fixset -(subnK (leq_ord x)) /iterF iterD iter_fix.
 apply: contraT => /existsPn /(_ (Ordinal _)) /= neq_iter.
 suff iter_big k : k <= n.+1 -> k <= #|iter k F set0|.
   by have := iter_big _ (leqnn _); rewrite ltnNge max_card.
@@ -2312,7 +2312,7 @@ Proof. by rewrite iter_fix. Qed.
 Lemma iter_sub_fix k : iterF k \subset fixset.
 Proof.
 have [/subset_iter //|/ltnW/subnK<-] := leqP k n;
-by rewrite /iterF iter_add fixsetKn.
+by rewrite /iterF iterD fixsetKn.
 Qed.
 
 Lemma fix_order_proof x : x \in fixset -> exists n, x \in iterF n.
@@ -2396,6 +2396,8 @@ End Greatest.
 End SetFixpoint.
 
 Notation mem_imset := 
-  ((fun aT rT D x f xD => deprecate mem_imset imset_f aT rT f D x xD) _ _ _ _).
+  ((fun aT rT D x f xD => deprecate mem_imset imset_f aT rT f D x xD) _ _ _ _)
+  (only parsing).
 Notation mem_imset2 := ((fun aT aT2 rT D D2 x x2 f xD xD2 => 
-  deprecate mem_imset2 imset2_f aT aT2 rT f D D2 x x2 xD xD2) _ _ _ _ _ _ _).
+  deprecate mem_imset2 imset2_f aT aT2 rT f D D2 x x2 xD xD2) _ _ _ _ _ _ _)
+  (only parsing).
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 726b8c2..422d760 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -2041,20 +2041,20 @@ Qed.
 Lemma unbumpK {h} : {in predC1 h, cancel (unbump h) (bump h)}.
 Proof. by move=> i /negbTE-neq_h_i; rewrite unbumpKcond neq_h_i. Qed.
 
-Lemma bump_addl h i k : bump (k + h) (k + i) = k + bump h i.
+Lemma bumpDl h i k : bump (k + h) (k + i) = k + bump h i.
 Proof. by rewrite /bump leq_add2l addnCA. Qed.
 
 Lemma bumpS h i : bump h.+1 i.+1 = (bump h i).+1.
 Proof. exact: addnS. Qed.
 
-Lemma unbump_addl h i k : unbump (k + h) (k + i) = k + unbump h i.
+Lemma unbumpDl h i k : unbump (k + h) (k + i) = k + unbump h i.
 Proof.
 apply: (can_inj (bumpK (k + h))).
-by rewrite bump_addl !unbumpKcond eqn_add2l addnCA.
+by rewrite bumpDl !unbumpKcond eqn_add2l addnCA.
 Qed.
 
 Lemma unbumpS h i : unbump h.+1 i.+1 = (unbump h i).+1.
-Proof. exact: unbump_addl 1. Qed.
+Proof. exact: unbumpDl 1. Qed.
 
 Lemma leq_bump h i j : (i <= bump h j) = (unbump h i <= j).
 Proof.
@@ -2238,7 +2238,7 @@ Proof. by rewrite /inord /insubd valK. Qed.
 Lemma enum_ordS : enum 'I_n = ord0 :: map (lift ord0) (enum 'I_n').
 Proof.
 apply: (inj_map val_inj); rewrite val_enum_ord /= -map_comp.
-by rewrite (map_comp (addn 1)) val_enum_ord -iota_addl.
+by rewrite (map_comp (addn 1)) val_enum_ord -iotaDl.
 Qed.
 
 Lemma lift_max (i : 'I_n') : lift ord_max i = i :> nat.
@@ -2345,3 +2345,6 @@ Lemma card_sum : #|{: T1 + T2}| = #|T1| + #|T2|.
 Proof. by rewrite !cardT !enumT [in LHS]unlock size_cat !size_map. Qed.
 
 End SumFinType.
+
+Notation bump_addl := (deprecate bump_addl bumpDl) (only parsing).
+Notation unbump_addl := (deprecate unbump_addl unbumpDl) (only parsing).
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index 7d1f0e9..0965b14 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -865,7 +865,7 @@ apply: ihss.
   rewrite (perm_mem perm_s2) mem_iota => /andP [] _ hy'.
   apply/allP => n; rewrite (perm_mem perm_s1) mem_iota => /andP [].
   by rewrite -cat_cons size_cat addnC => /(leq_trans hy').
-- rewrite /= perm_ss andbT perm_merge size_merge size_cat iota_add perm_cat //.
+- rewrite /= perm_ss andbT perm_merge size_merge size_cat iotaD perm_cat //.
   by rewrite addnC -size_cat.
 Qed.
 
@@ -880,7 +880,7 @@ apply: ihss => /=.
   apply/allP => m'; rewrite (perm_mem perm_s2) mem_iota => /andP [_ hm'].
   apply/allP => n; rewrite (perm_mem perm_s1) mem_iota -cat_cons size_cat.
   by rewrite addnC => /andP [] /(leq_trans hm').
-- rewrite perm_ss andbT perm_merge size_merge size_cat iota_add perm_cat //.
+- rewrite perm_ss andbT perm_merge size_merge size_cat iotaD perm_cat //.
   by rewrite addnC -size_cat.
 Qed.
 
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 2f35e35..8e94ef6 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -269,8 +269,8 @@ case def_d: d if_d0 => [|d'] => [[//|{def_m ltdp pr_p} def_m pr_p pr_m'] | _].
   rewrite -addnA -doubleD addnCA def_a addSnnS def_k1 -(addnC k) -mulnSr.
   by rewrite -[_.*2.+1]/p mulnDl doubleD addnA -mul2n mulnA mul2n -mulSn.
 have next_pm: lb_dvd p.+2 m.
-  rewrite /lb_dvd /index_iota 2!subSS subn0 -(subnK lt1p) iota_add.
-  rewrite has_cat; apply/norP; split=> //=; rewrite orbF subnKC // orbC.
+  rewrite /lb_dvd /index_iota (addKn 2) -(subnK lt1p) iotaD has_cat.
+  apply/norP; split; rewrite //= orbF subnKC // orbC.
   apply/norP; split; apply/dvdnP=> [[q def_q]].
      case/hasP: leppm; exists 2; first by rewrite /p -(subnKC lt0k).
     by rewrite /= def_q dvdn_mull // dvdn2 /= odd_double.
@@ -549,18 +549,18 @@ Arguments primePns {n}.
 Lemma pdivP n : n > 1 -> {p | prime p & p %| n}.
 Proof. by move=> lt1n; exists (pdiv n); rewrite ?pdiv_dvd ?pdiv_prime. Qed.
 
-Lemma primes_mul m n p : m > 0 -> n > 0 ->
+Lemma primesM m n p : m > 0 -> n > 0 ->
   (p \in primes (m * n)) = (p \in primes m) || (p \in primes n).
 Proof.
 move=> m_gt0 n_gt0; rewrite !mem_primes muln_gt0 m_gt0 n_gt0.
 by case pr_p: (prime p); rewrite // Euclid_dvdM.
 Qed.
 
-Lemma primes_exp m n : n > 0 -> primes (m ^ n) = primes m.
+Lemma primesX m n : n > 0 -> primes (m ^ n) = primes m.
 Proof.
 case: n => // n _; rewrite expnS; have [-> // | m_gt0] := posnP m.
 apply/eq_primes => /= p; elim: n => [|n IHn]; first by rewrite muln1.
-by rewrite primes_mul ?(expn_gt0, expnS, IHn, orbb, m_gt0).
+by rewrite primesM ?(expn_gt0, expnS, IHn, orbb, m_gt0).
 Qed.
 
 Lemma primes_prime p : prime p -> primes p = [::p].
@@ -588,7 +588,7 @@ Lemma pdiv_id p : prime p -> pdiv p = p.
 Proof. by move=> p_pr; rewrite /pdiv primes_prime. Qed.
 
 Lemma pdiv_pfactor p k : prime p -> pdiv (p ^ k.+1) = p.
-Proof. by move=> p_pr; rewrite /pdiv primes_exp ?primes_prime. Qed.
+Proof. by move=> p_pr; rewrite /pdiv primesX ?primes_prime. Qed.
 
 (* Primes are unbounded. *)
 
@@ -707,7 +707,7 @@ have [m0 | m_gt0] := posnP m; first by rewrite m0 prime_coprime ?dvdn0 in co_pm.
 have mn_gt0: m * n > 0 by rewrite muln_gt0 m_gt0.
 apply/eqP; rewrite eqn_leq andbC dvdn_leq_log ?dvdn_mull //.
 set k := logn p _; have: p ^ k %| m * n by rewrite pfactor_dvdn.
-by rewrite Gauss_dvdr ?coprime_expl // -pfactor_dvdn.
+by rewrite Gauss_dvdr ?coprimeXl // -pfactor_dvdn.
 Qed.
 
 Lemma logn_coprime p m : coprime p m -> logn p m = 0.
@@ -747,7 +747,7 @@ exists (logn p d); first by rewrite -(pfactorK n p_pr) dvdn_leq_log.
 have d_gt0: d > 0 by apply: dvdn_gt0 dv_d_pn.
 case: (pfactor_coprime p_pr d_gt0) => q co_p_q def_d.
 rewrite [LHS]def_d ((q =P 1) _) ?mul1n // -dvdn1.
-suff: q %| p ^ n * 1 by rewrite Gauss_dvdr // coprime_sym coprime_expl.
+suff: q %| p ^ n * 1 by rewrite Gauss_dvdr // coprime_sym coprimeXl.
 by rewrite muln1 (dvdn_trans _ dv_d_pn) // def_d dvdn_mulr.
 Qed.
 
@@ -762,7 +762,7 @@ case/mem_prime_decomp=> pr_p _ _.
 rewrite (big_nth f0) big_mkord (bigD1 (Ordinal lt_i_n)) //=.
 rewrite def_f mulnC logn_Gauss ?pfactorK //.
 apply big_ind => [|m1 m2 com1 com2| [j ltj] /=]; first exact: coprimen1.
-  by rewrite coprime_mulr com1.
+  by rewrite coprimeMr com1.
 rewrite -val_eqE /= => nji; case def_j: (nth _ _ j) => [q e1] /=.
 have: (q, e1) \in prime_decomp n.+1 by rewrite -def_j mem_nth.
 case/mem_prime_decomp=> pr_q e1_gt0 _; rewrite coprime_pexpr //.
@@ -1092,17 +1092,17 @@ Proof. exact: eq_pnat (negnK pi). Qed.
 Lemma pnatI pi rho n : [predI pi & rho].-nat n = pi.-nat n && rho.-nat n.
 Proof. by rewrite /pnat andbCA all_predI !andbA andbb. Qed.
 
-Lemma pnat_mul pi m n : pi.-nat (m * n) = pi.-nat m && pi.-nat n.
+Lemma pnatM pi m n : pi.-nat (m * n) = pi.-nat m && pi.-nat n.
 Proof.
 rewrite /pnat muln_gt0 andbCA -andbA andbCA.
 case: posnP => // n_gt0; case: posnP => //= m_gt0.
 apply/allP/andP=> [pi_mn | [pi_m pi_n] p].
-  by split; apply/allP=> p m_p; apply: pi_mn; rewrite primes_mul // m_p ?orbT.
-by rewrite primes_mul // => /orP[]; [apply: (allP pi_m) | apply: (allP pi_n)].
+  by split; apply/allP=> p m_p; apply: pi_mn; rewrite primesM // m_p ?orbT.
+by rewrite primesM // => /orP[]; [apply: (allP pi_m) | apply: (allP pi_n)].
 Qed.
 
-Lemma pnat_exp pi m n : pi.-nat (m ^ n) = pi.-nat m || (n == 0).
-Proof. by case: n => [|n]; rewrite orbC // /pnat expn_gt0 orbC primes_exp. Qed.
+Lemma pnatX pi m n : pi.-nat (m ^ n) = pi.-nat m || (n == 0).
+Proof. by case: n => [|n]; rewrite orbC // /pnat expn_gt0 orbC primesX. Qed.
 
 Lemma part_pnat pi n : pi.-nat n`_pi.
 Proof.
@@ -1131,13 +1131,13 @@ exact: dvdn_trans p_dv_m m_dv_n.
 Qed.
 
 Lemma pi_ofM m n : m > 0 -> n > 0 -> \pi(m * n) =i [predU \pi(m) & \pi(n)].
-Proof. by move=> m_gt0 n_gt0 p; apply: primes_mul. Qed.
+Proof. by move=> m_gt0 n_gt0 p; apply: primesM. Qed.
 
 Lemma pi_of_part pi n : n > 0 -> \pi(n`_pi) =i [predI \pi(n) & pi].
 Proof. by move=> n_gt0 p; rewrite /pi_of primes_part mem_filter andbC. Qed.
 
 Lemma pi_of_exp p n : n > 0 -> \pi(p ^ n) = \pi(p).
-Proof. by move=> n_gt0; rewrite /pi_of primes_exp. Qed.
+Proof. by move=> n_gt0; rewrite /pi_of primesX. Qed.
 
 Lemma pi_of_prime p : prime p -> \pi(p) =i (p : nat_pred).
 Proof. by move=> pr_p q; rewrite /pi_of primes_prime // mem_seq1. Qed.
@@ -1155,11 +1155,11 @@ Lemma pnatPpi pi n p : pi.-nat n -> p \in \pi(n) -> p \in pi.
 Proof. by case/andP=> _ /allP; apply. Qed.
 
 Lemma pnat_dvd m n pi : m %| n -> pi.-nat n -> pi.-nat m.
-Proof. by case/dvdnP=> q ->; rewrite pnat_mul; case/andP. Qed.
+Proof. by case/dvdnP=> q ->; rewrite pnatM; case/andP. Qed.
 
 Lemma pnat_div m n pi : m %| n -> pi.-nat n -> pi.-nat (n %/ m).
 Proof.
-case/dvdnP=> q ->; rewrite pnat_mul andbC => /andP[].
+case/dvdnP=> q ->; rewrite pnatM andbC => /andP[].
 by case: m => // m _; rewrite mulnK.
 Qed.
 
@@ -1295,7 +1295,7 @@ rewrite mem_merge mem_cat; case dv_d_p: (p %| d).
 case pdiv_d: (_ \in _).
   by case/mapP: pdiv_d dv_d_p => d' _ ->; rewrite natTrecE dvdn_mulr.
 rewrite mem_divs Gauss_dvdr // coprime_sym.
-by rewrite coprime_expl ?prime_coprime ?dv_d_p.
+by rewrite coprimeXl ?prime_coprime ?dv_d_p.
 Qed.
 
 Lemma sorted_divisors n : sorted leq (divisors n).
@@ -1365,7 +1365,7 @@ Lemma totient_pfactor p e :
   prime p -> e > 0 -> totient (p ^ e) = p.-1 * p ^ e.-1.
 Proof.
 move=> p_pr e_gt0; rewrite totientE ?expn_gt0 ?prime_gt0 //.
-by rewrite primes_exp // primes_prime // unlock /= muln1 pfactorK.
+by rewrite primesX // primes_prime // unlock /= muln1 pfactorK.
 Qed.
 
 Lemma totient_prime p : prime p -> totient p = p.-1.
@@ -1380,13 +1380,13 @@ rewrite !totientE ?muln_gt0 ?m_gt0 //.
 have /(perm_big _)->: perm_eq (primes (m * n)) (primes m ++ primes n).
   apply: uniq_perm => [||p]; first exact: primes_uniq.
     by rewrite cat_uniq !primes_uniq -coprime_has_primes // co_mn.
-  by rewrite mem_cat primes_mul.
+  by rewrite mem_cat primesM.
 rewrite big_cat /= !big_seq.
 congr (_ * _); apply: eq_bigr => p; rewrite mem_primes => /and3P[_ _ dvp].
   rewrite (mulnC m) logn_Gauss //; move: co_mn.
-  by rewrite -(divnK dvp) coprime_mull => /andP[].
+  by rewrite -(divnK dvp) coprimeMl => /andP[].
 rewrite logn_Gauss //; move: co_mn.
-by rewrite coprime_sym -(divnK dvp) coprime_mull => /andP[].
+by rewrite coprime_sym -(divnK dvp) coprimeMl => /andP[].
 Qed.
 
 Lemma totient_count_coprime n : totient n = \sum_(0 <= d < n) coprime n d.
@@ -1422,9 +1422,17 @@ have ->: totient np = #|[pred d : 'I_np | coprime np d]|.
 pose h (d : 'I_n) := (in_mod _ np0 d, in_mod _ np'0 d).
 pose h' (d : 'I_np * 'I_np') := in_mod _ n0 (chinese np np' d.1 d.2).
 rewrite -!big_mkcond -sum_nat_const pair_big (reindex_onto h h') => [|[d d'] _].
-  apply: eq_bigl => [[d ltd] /=]; rewrite !inE /= -val_eqE /= andbC.
-  rewrite !coprime_modr def_n -chinese_mod // -coprime_mull -def_n.
-  by rewrite modn_small ?eqxx.
+  apply: eq_bigl => [[d ltd] /=]; rewrite !inE -val_eqE /= andbC !coprime_modr.
+  by rewrite def_n -chinese_mod // -coprimeMl -def_n modn_small ?eqxx.
 apply/eqP; rewrite /eq_op /= /eq_op /= !modn_dvdm ?dvdn_part //.
 by rewrite chinese_modl // chinese_modr // !modn_small ?eqxx ?ltn_ord.
 Qed.
+
+Notation "@ 'primes_mul'" :=
+  (deprecate primes_mul primesM) (at level 10, only parsing) : fun_scope.
+Notation "@ 'primes_exp'" :=
+  (deprecate primes_exp primesX) (at level 10, only parsing) : fun_scope.
+Notation primes_mul := (@primes_mul _ _) (only parsing).
+Notation primes_exp := (fun m => @primes_exp m _) (only parsing).
+Notation pnat_mul := (deprecate pnat_mul pnatM) (only parsing).
+Notation pnat_exp := (deprecate pnat_exp pnatX) (only parsing).
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 15f9421..7cdc422 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -284,9 +284,8 @@ Lemma cat_cons x s1 s2 : (x :: s1) ++ s2 = x :: s1 ++ s2. Proof. by []. Qed.
 Lemma cat_nseq n x s : nseq n x ++ s = ncons n x s.
 Proof. by elim: n => //= n ->. Qed.
 
-Lemma nseqD n1 n2 x :
-  nseq (n1 + n2) x = nseq n1 x ++ nseq n2 x.
-Proof. by rewrite cat_nseq /nseq /ncons iter_add. Qed.
+Lemma nseqD n1 n2 x : nseq (n1 + n2) x = nseq n1 x ++ nseq n2 x.
+Proof. by rewrite cat_nseq /nseq /ncons iterD. Qed.
 
 Lemma cats0 s : s ++ [::] = s.
 Proof. by elim: s => //= x s ->. Qed.
@@ -2504,15 +2503,15 @@ Fixpoint iota m n := if n is n'.+1 then m :: iota m.+1 n' else [::].
 Lemma size_iota m n : size (iota m n) = n.
 Proof. by elim: n m => //= n IHn m; rewrite IHn. Qed.
 
-Lemma iota_add m n1 n2 : iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2.
+Lemma iotaD m n1 n2 : iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2.
 Proof. by elim: n1 m => [|n1 IHn1] m; rewrite ?addn0 // -addSnnS /= -IHn1. Qed.
 
-Lemma iota_addl m1 m2 n : iota (m1 + m2) n = map (addn m1) (iota m2 n).
+Lemma iotaDl m1 m2 n : iota (m1 + m2) n = map (addn m1) (iota m2 n).
 Proof. by elim: n m2 => //= n IHn m2; rewrite -addnS IHn. Qed.
 
 Lemma nth_iota p m n i : i < n -> nth p (iota m n) i = m + i.
 Proof.
-by move/subnKC <-; rewrite addSnnS iota_add nth_cat size_iota ltnn subnn.
+by move/subnKC <-; rewrite addSnnS iotaD nth_cat size_iota ltnn subnn.
 Qed.
 
 Lemma mem_iota m n i : (i \in iota m n) = (m <= i < m + n).
@@ -2583,7 +2582,7 @@ elim: t => [|x t IHt] in s It Est *.
 have /rot_to[k s1 Ds]: x \in s by rewrite (perm_mem Est) mem_head.
 have [|Is1 eqIst1 Ds1] := IHt s1; first by rewrite -(perm_cons x) -Ds perm_rot.
 exists (rotr k (0 :: map succn Is1)).
-  by rewrite perm_rot /It /= perm_cons (iota_addl 1) perm_map.
+  by rewrite perm_rot /It /= perm_cons (iotaDl 1) perm_map.
 by rewrite map_rotr /= -map_comp -(@eq_map _ _ (nth x0 t)) // -Ds1 -Ds rotK.
 Qed.
 
@@ -3581,3 +3580,6 @@ Notation uniq_perm_eq := (deprecate uniq_perm_eq uniq_perm _ _ _)
 Notation perm_eq_iotaP := (deprecate perm_eq_iotaP perm_iotaP) (only parsing).
 Notation perm_undup_count := (deprecate perm_undup_count perm_count_undup _ _)
   (only parsing).
+
+Notation iota_add := (deprecate iota_add iotaD) (only parsing).
+Notation iota_addl := (deprecate iota_addl iotaDl) (only parsing).
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 8b88821..9f17eb9 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -939,7 +939,7 @@ Proof. by elim: n => //= n <-. Qed.
 
 Lemma iterS n f x : iter n.+1 f x = f (iter n f x). Proof. by []. Qed.
 
-Lemma iter_add n m f x : iter (n + m) f x = iter n f (iter m f x).
+Lemma iterD n m f x : iter (n + m) f x = iter n f (iter m f x).
 Proof. by elim: n => //= n ->. Qed.
 
 Lemma iteriS n f x : iteri n.+1 f x = f n (iteri n f x).
@@ -1114,17 +1114,17 @@ move=> lt_mn1 lt_mn2; apply (@leq_ltn_trans (m1 * n2)).
 by rewrite ltn_pmul2r // (leq_trans _ lt_mn2).
 Qed.
 
-Lemma maxn_mulr : right_distributive muln maxn.
+Lemma maxnMr : right_distributive muln maxn.
 Proof. by case=> // m n1 n2; rewrite /maxn (fun_if (muln _)) ltn_pmul2l. Qed.
 
-Lemma maxn_mull : left_distributive muln maxn.
-Proof. by move=> m1 m2 n; rewrite -!(mulnC n) maxn_mulr. Qed.
+Lemma maxnMl : left_distributive muln maxn.
+Proof. by move=> m1 m2 n; rewrite -!(mulnC n) maxnMr. Qed.
 
-Lemma minn_mulr : right_distributive muln minn.
+Lemma minnMr : right_distributive muln minn.
 Proof. by case=> // m n1 n2; rewrite /minn (fun_if (muln _)) ltn_pmul2l. Qed.
 
-Lemma minn_mull : left_distributive muln minn.
-Proof. by move=> m1 m2 n; rewrite -!(mulnC n) minn_mulr. Qed.
+Lemma minnMl : left_distributive muln minn.
+Proof. by move=> m1 m2 n; rewrite -!(mulnC n) minnMr. Qed.
 
 (* Exponentiation. *)
 
@@ -1276,14 +1276,14 @@ Proof.
 by move=> le_nm; apply: (@canRL bool) (addbK _) _; rewrite -oddD subnK.
 Qed.
 
-Lemma odd_opp i m : odd m = false -> i <= m -> odd (m - i) = odd i.
-Proof. by move=> oddm le_im; rewrite (oddB (le_im)) oddm. Qed.
+Lemma oddN i m : odd m = false -> i <= m -> odd (m - i) = odd i.
+Proof. by move=> oddm /oddB ->; rewrite oddm. Qed.
 
-Lemma odd_mul m n : odd (m * n) = odd m && odd n.
+Lemma oddM m n : odd (m * n) = odd m && odd n.
 Proof. by elim: m => //= m IHm; rewrite oddD -addTb andb_addl -IHm. Qed.
 
-Lemma odd_exp m n : odd (m ^ n) = (n == 0) || odd m.
-Proof. by elim: n => // n IHn; rewrite expnS odd_mul {}IHn orbC; case odd. Qed.
+Lemma oddX m n : odd (m ^ n) = (n == 0) || odd m.
+Proof. by elim: n => // n IHn; rewrite expnS oddM {}IHn orbC; case odd. Qed.
 
 (* Doubling. *)
 
@@ -1405,7 +1405,7 @@ rewrite -!mulnn mul2n mulnDr !mulnDl (mulnC n) -!addnA.
 by congr (_ + _); rewrite addnA addnn addnC.
 Qed.
 
-Lemma sqrn_sub m n : n <= m -> (m - n) ^ 2 = m ^ 2 + n ^ 2 - 2 * (m * n).
+Lemma sqrnB m n : n <= m -> (m - n) ^ 2 = m ^ 2 + n ^ 2 - 2 * (m * n).
 Proof.
 move/subnK <-; rewrite addnK sqrnD -addnA -addnACA -addnA.
 by rewrite addnn -mul2n -mulnDr -mulnDl addnK.
@@ -1414,7 +1414,7 @@ Qed.
 Lemma sqrnD_sub m n : n <= m -> (m + n) ^ 2 - 4 * (m * n) = (m - n) ^ 2.
 Proof.
 move=> le_nm; rewrite -[4]/(2 * 2) -mulnA mul2n -addnn subnDA.
-by rewrite sqrnD addnK sqrn_sub.
+by rewrite sqrnD addnK sqrnB.
 Qed.
 
 Lemma subn_sqr m n : m ^ 2 - n ^ 2 = (m - n) * (m + n).
@@ -1516,7 +1516,7 @@ Proof.
 without loss le_nm: m n / n <= m.
   by have [?|/ltnW ?] := leqP n m; last rewrite eq_sym addnC (mulnC m); apply.
 apply/leqifP; have [-> | ne_mn] := eqVneq; first by rewrite addnn mul2n.
-by rewrite -subn_gt0 -sqrn_sub // sqrn_gt0 subn_gt0 ltn_neqAle eq_sym ne_mn.
+by rewrite -subn_gt0 -sqrnB // sqrn_gt0 subn_gt0 ltn_neqAle eq_sym ne_mn.
 Qed.
 
 Lemma nat_AGM2 m n : 4 * (m * n) <= (m + n) ^ 2 ?= iff (m == n).
@@ -2035,3 +2035,19 @@ Notation decr_inj := (@decr_inj _) (only parsing).
 Notation "@ 'decr_inj_in'" :=
   (deprecate decr_inj_in decn_inj_in) (at level 10, only parsing) : fun_scope.
 Notation decr_inj_in := (@decr_inj_in _ _) (only parsing).
+
+Notation "@ 'iter_add'" :=
+  (deprecate iter_add iterD) (at level 10, only parsing) : fun_scope.
+Notation "@ 'odd_opp'" :=
+  (deprecate odd_opp oddN) (at level 10, only parsing) : fun_scope.
+Notation "@ 'sqrn_sub'" :=
+  (deprecate sqrn_sub sqrnB) (at level 10, only parsing) : fun_scope.
+Notation iter_add := (@iter_add _) (only parsing).
+Notation maxn_mulr := (deprecate maxn_mulr maxnMr) (only parsing).
+Notation maxn_mull := (deprecate maxn_mull maxnMl) (only parsing).
+Notation minn_mulr := (deprecate minn_mulr minnMr) (only parsing).
+Notation minn_mull := (deprecate minn_mull minnMl) (only parsing).
+Notation odd_opp := (@odd_opp _ _) (only parsing).
+Notation odd_mul := (deprecate odd_mul oddM) (only parsing).
+Notation odd_exp := (deprecate odd_exp oddX) (only parsing).
+Notation sqrn_sub := (@sqrn_sub _ _) (only parsing).