Switch from long suffixes to short suffixes

11 files changed, 279 insertions, 151 deletions

diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index 808d21d..336b6df 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.v
@@ -601,11 +601,11 @@ Proof. by rewrite /gcdz abszM => /Gauss_gcdr->. Qed.
 Lemma Gauss_gcdzl p m n : coprimez p n -> gcdz p (m * n) = gcdz p m.
 Proof. by move=> co_pn; rewrite mulrC Gauss_gcdzr. Qed.
 
-Lemma coprimez_mulr p m n : coprimez p (m * n) = coprimez p m && coprimez p n.
-Proof. by rewrite -coprime_mulr -abszM. Qed.
+Lemma coprimezMr p m n : coprimez p (m * n) = coprimez p m && coprimez p n.
+Proof. by rewrite -coprimeMr -abszM. Qed.
 
-Lemma coprimez_mull p m n : coprimez (m * n) p = coprimez m p && coprimez n p.
-Proof. by rewrite -coprime_mull -abszM. Qed.
+Lemma coprimezMl p m n : coprimez (m * n) p = coprimez m p && coprimez n p.
+Proof. by rewrite -coprimeMl -abszM. Qed.
 
 Lemma coprimez_pexpl k m n : (0 < k)%N -> coprimez (m ^+ k) n = coprimez m n.
 Proof. by rewrite /coprimez /gcdz abszX; apply: coprime_pexpl. Qed.
@@ -613,11 +613,11 @@ Proof. by rewrite /coprimez /gcdz abszX; apply: coprime_pexpl. Qed.
 Lemma coprimez_pexpr k m n : (0 < k)%N -> coprimez m (n ^+ k) = coprimez m n.
 Proof. by move=> k_gt0; rewrite !(coprimez_sym m) coprimez_pexpl. Qed.
 
-Lemma coprimez_expl k m n : coprimez m n -> coprimez (m ^+ k) n.
-Proof. by rewrite /coprimez /gcdz abszX; apply: coprime_expl. Qed.
+Lemma coprimezXl k m n : coprimez m n -> coprimez (m ^+ k) n.
+Proof. by rewrite /coprimez /gcdz abszX; apply: coprimeXl. Qed.
 
-Lemma coprimez_expr k m n : coprimez m n -> coprimez m (n ^+ k).
-Proof. by rewrite !(coprimez_sym m); apply: coprimez_expl. Qed.
+Lemma coprimezXr k m n : coprimez m n -> coprimez m (n ^+ k).
+Proof. by rewrite !(coprimez_sym m); apply: coprimezXl. Qed.
 
 Lemma coprimez_dvdl m n p : (m %| n)%N -> coprimez n p -> coprimez m p.
 Proof. exact: coprime_dvdl. Qed.
@@ -878,7 +878,7 @@ Lemma dvdpP_rat_int p q :
   {p1 : {poly int} & {a | a != 0 & p = a *: pZtoQ p1} & {r | q = p1 * r}}.
 Proof.
 have{p} [p [a nz_a ->]] := rat_poly_scale p.
-rewrite dvdp_scalel ?invr_eq0 ?intr_eq0 // dvdp_rat_int => dv_p_q.
+rewrite dvdpZl ?invr_eq0 ?intr_eq0 // dvdp_rat_int => dv_p_q.
 exists (zprimitive p); last exact: dvdpP_int.
 have [-> | nz_p] := eqVneq p 0.
   by exists 1; rewrite ?oner_eq0 // zprimitive0 map_poly0 !scaler0.
@@ -1074,3 +1074,12 @@ rewrite -defS -2!mulmxA; have ->: T *m pinvmx T = 1%:M.
   by apply: (row_free_inj uT); rewrite mul1mx mulmxKpV.
 by move=> i; rewrite mulmx1 -map_mxM 2!mxE denq_int mxE.
 Qed.
+
+Notation "@ 'coprimez_expl'" :=
+  (deprecate coprimez_expl coprimezXl) (at level 10, only parsing) : fun_scope.
+Notation "@ 'coprimez_expr'" :=
+  (deprecate coprimez_expr coprimezXr) (at level 10, only parsing) : fun_scope.
+Notation coprimez_mull := (deprecate coprimez_mull coprimezMl) (only parsing).
+Notation coprimez_mulr := (deprecate coprimez_mulr coprimezMr) (only parsing).
+Notation coprimez_expl := (fun k => @coprimez_expl k _ _) (only parsing).
+Notation coprimez_expr := (fun k => @coprimez_expr k _ _) (only parsing).
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index feb9edd..f7d7730 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -1699,12 +1699,12 @@ Proof. by apply/matrixP=> i j; rewrite !mxE raddfN. Qed.
 Lemma map_mxD A B : (A + B)^f = A^f + B^f.
 Proof. by apply/matrixP=> i j; rewrite !mxE raddfD. Qed.
 
-Lemma map_mx_sub A B : (A - B)^f = A^f - B^f.
+Lemma map_mxB A B : (A - B)^f = A^f - B^f.
 Proof. by rewrite map_mxD map_mxN. Qed.
 
 Definition map_mx_sum := big_morph _ map_mxD map_mx0.
 
-Canonical map_mx_additive := Additive map_mx_sub.
+Canonical map_mx_additive := Additive map_mxB.
 
 End MapZmodMatrix.
 
@@ -2691,7 +2691,7 @@ Proof. by apply/matrixP=> i j; rewrite !mxE cofactor_map_mx. Qed.
 End FixedSize.
 
 Lemma map_copid_mx n r : (copid_mx r)^f = copid_mx r :> 'M_n.
-Proof. by rewrite map_mx_sub map_mx1 map_pid_mx. Qed.
+Proof. by rewrite map_mxB map_mx1 map_pid_mx. Qed.
 
 Lemma map_mx_is_multiplicative n' (n := n'.+1) :
   multiplicative (map_mx f : 'M_n -> 'M_n).
@@ -3687,3 +3687,7 @@ Canonical mxOver_subringPred (S : {pred R}) (ringS : subringPred S)
 
 End mxRingOver.
 End mxOver.
+
+Notation "@ 'map_mx_sub'" :=
+  (deprecate map_mx_sub map_mxB) (at level 10, only parsing) : fun_scope.
+Notation map_mx_sub := (fun f => @map_mx_sub _ _ f) (only parsing).
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index 7e213b8..e65bc3c 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -2581,8 +2581,8 @@ rewrite mulmx_suml linear_sum summx_sub //= => i _.
 by rewrite -mulmxA !mem_mulsmx.
 Qed.
 
-Lemma mulsmx_addl m1 m2 m3 n
-                 (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) :
+Lemma mulsmxDl m1 m2 m3 n
+               (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) :
   ((R1 + R2) * R3 = R1 * R3 + R2 * R3)%MS.
 Proof.
 rewrite -(genmx_muls R2 R3) -(genmx_muls R1 R3) -genmx_muls -genmx_adds.
@@ -2591,8 +2591,8 @@ apply/mulsmx_subP=> _ A3 /memmx_addsP[A [R_A1 R_A2 ->]] R_A3.
 by rewrite mulmxDl linearD addmx_sub_adds ?mem_mulsmx.
 Qed.
 
-Lemma mulsmx_addr m1 m2 m3 n
-                  (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) :
+Lemma mulsmxDr m1 m2 m3 n
+               (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) :
   (R1 * (R2 + R3) = R1 * R2 + R1 * R3)%MS.
 Proof.
 rewrite -(genmx_muls R1 R3) -(genmx_muls R1 R2) -genmx_muls -genmx_adds.
@@ -2857,7 +2857,7 @@ set pAnz := [pred k | A k.1 k.2 != 0].
 rewrite (@eq_pick _ _ pAnz) => [|k]; last by rewrite /= mxE fmorph_eq0.
 case: {+}(pick _) => [[i j]|]; last by rewrite !map_mx1.
 rewrite mxE -fmorphV  -map_xcol -map_xrow -map_dlsubmx -map_drsubmx.
-rewrite -map_ursubmx -map_mxZ -map_mxM -map_mx_sub {}IHm /=.
+rewrite -map_ursubmx -map_mxZ -map_mxM -map_mxB {}IHm /=.
 case: {+}(Gaussian_elimination _) => [[L U] r] /=; rewrite map_xrow map_xcol.
 by rewrite !(@map_block_mx _ _ f 1 _ 1) !map_mx0 ?map_mx1 ?map_scalar_mx.
 Qed.
@@ -2952,7 +2952,7 @@ by rewrite -!map_capmx !map_submx -!diffmxE andbb.
 Qed.
 
 Lemma map_eigenspace n (g : 'M_n) a : (eigenspace g a)^f = eigenspace g^f (f a).
-Proof. by rewrite map_kermx map_mx_sub ?map_scalar_mx. Qed.
+Proof. by rewrite map_kermx map_mxB ?map_scalar_mx. Qed.
 
 Lemma eigenvalue_map n (g : 'M_n) a : eigenvalue g^f (f a) = eigenvalue g a.
 Proof. by rewrite /eigenvalue -map_eigenspace map_mx_eq0. Qed.
@@ -2972,12 +2972,18 @@ Qed.
 
 Lemma map_cent_mx m n (E : 'A_(m, n)) : ('C(E)%MS)^f = 'C(E^f)%MS.
 Proof.
-rewrite map_kermx //; congr (kermx _); apply: map_lin_mx => // A.
-rewrite map_mxM //; congr (_ *m _); apply: map_lin_mx => //= B.
-by rewrite map_mx_sub ? map_mxM.
+rewrite map_kermx; congr kermx; apply: map_lin_mx => A; rewrite map_mxM.
+by congr (_ *m _); apply: map_lin_mx => B; rewrite map_mxB ?map_mxM.
 Qed.
 
 Lemma map_center_mx m n (E : 'A_(m, n)) : (('Z(E))^f :=: 'Z(E^f))%MS.
 Proof. by rewrite /center_mx -map_cent_mx; apply: map_capmx. Qed.
 
 End MapMatrixSpaces.
+
+Notation "@ 'mulsmx_addl'" :=
+  (deprecate mulsmx_addl mulsmxDl) (at level 10, only parsing) : fun_scope.
+Notation "@ 'mulsmx_addr'" :=
+  (deprecate mulsmx_addr mulsmxDr) (at level 10, only parsing) : fun_scope.
+Notation mulsmx_addl := (@mulsmx_addl _ _ _ _ _) (only parsing).
+Notation mulsmx_addr := (@mulsmx_addr _ _ _ _ _) (only parsing).
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index 74d524e..acf0e95 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -890,7 +890,7 @@ rewrite !big_cons; case: ifP => [Pj|PNj]; rewrite ?ihjs ?submx_refl//.
 suff cjjs: coprimep (p_ j) (\prod_(i <- js | P i) p_ i).
   by rewrite !kermxpolyM// !(adds_eqmx (eqmx_refl _) (ihjs _)) ?submx_refl.
 rewrite (@big_morph _ _ _ true andb) ?big_all_cond ?coprimep1//; last first.
-  by move=> p q; rewrite coprimep_mulr.
+  by move=> p q; rewrite coprimepMr.
 apply/allP => i i_js; apply/implyP => Pi; apply: p_coprime => //.
 by apply: contraNneq jNjs => <-.
 Qed.
@@ -907,7 +907,7 @@ have cpNi : {in [pred j | P j && (j != i)] &,
 rewrite -!(cap_eqmx (eqmx_refl _) (kermxpoly_prod g _))//.
 rewrite mxdirect_kermxpoly ?submx_refl//.
 rewrite (@big_morph _ _ _ true andb) ?big_all_cond ?coprimep1//; last first.
-  by move=> p q; rewrite coprimep_mulr.
+  by move=> p q; rewrite coprimepMr.
 by apply/allP => j _; apply/implyP => /andP[Pj neq_ji]; apply: p_coprime.
 Qed.
 
@@ -938,7 +938,7 @@ Lemma mxdirect_sum_geigenspace
   {in P &, injective a_} -> mxdirect (\sum_(i | P i) geigenspace g (a_ i)).
 Proof.
 move=> /inj_in_eq eq_a; apply: mxdirect_sum_kermx => i j Pi Pj Nji.
-by rewrite coprimep_expr ?coprimep_expl// coprimep_XsubC root_XsubC eq_a.
+by rewrite coprimepXr ?coprimepXl// coprimep_XsubC root_XsubC eq_a.
 Qed.
 
 Definition eigenpoly n (g : 'M_n) : pred {poly K} :=
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index a33788d..a95c776 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -428,26 +428,25 @@ Lemma coef_sum I (r : seq I) (P : pred I) (F : I -> {poly R}) k :
   (\sum_(i <- r | P i) F i)`_k = \sum_(i <- r | P i) (F i)`_k.
 Proof. exact: (raddf_sum (coefp_additive k)). Qed.
 
-Lemma polyC_add : {morph polyC : a b / a + b}.
+Lemma polyCD : {morph polyC : a b / a + b}.
 Proof. by move=> a b; apply/polyP=> [[|i]]; rewrite coefD !coefC ?addr0. Qed.
 
-Lemma polyC_opp : {morph polyC : c / - c}.
+Lemma polyCN : {morph polyC : c / - c}.
 Proof. by move=> c; apply/polyP=> [[|i]]; rewrite coefN !coefC ?oppr0. Qed.
 
-Lemma polyC_sub : {morph polyC : a b / a - b}.
-Proof. by move=> a b; rewrite polyC_add polyC_opp. Qed.
+Lemma polyCB : {morph polyC : a b / a - b}.
+Proof. by move=> a b; rewrite polyCD polyCN. Qed.
 
-Canonical polyC_additive := Additive polyC_sub.
+Canonical polyC_additive := Additive polyCB.
 
-Lemma polyC_muln n : {morph polyC : c / c *+ n}.
-Proof. exact: raddfMn. Qed.
+Lemma polyCMn n : {morph polyC : c / c *+ n}. Proof. exact: raddfMn. Qed.
 
 Lemma size_opp p : size (- p) = size p.
 Proof.
 by apply/eqP; rewrite eqn_leq -{3}(opprK p) -[-%R]/opp_poly unlock !size_poly.
 Qed.
 
-Lemma lead_coef_opp p : lead_coef (- p) = - lead_coef p.
+Lemma lead_coefN p : lead_coef (- p) = - lead_coef p.
 Proof. by rewrite /lead_coef size_opp coefN. Qed.
 
 Lemma size_add p q : size (p + q) <= maxn (size p) (size q).
@@ -621,15 +620,14 @@ rewrite coefMr big_ord_recl subn0.
 by rewrite big1 => [|j _]; rewrite coefC !simp.
 Qed.
 
-Lemma polyC_mul : {morph polyC : a b / a * b}.
+Lemma polyCM : {morph polyC : a b / a * b}.
 Proof. by move=> a b; apply/polyP=> [[|i]]; rewrite coefCM !coefC ?simp. Qed.
 
 Fact polyC_multiplicative : multiplicative polyC.
-Proof. by split; first apply: polyC_mul. Qed.
+Proof. by split; first apply: polyCM. Qed.
 Canonical polyC_rmorphism := AddRMorphism polyC_multiplicative.
 
-Lemma polyC_exp n : {morph polyC : c / c ^+ n}.
-Proof. exact: rmorphX. Qed.
+Lemma polyCX n : {morph polyC : c / c ^+ n}. Proof. exact: rmorphX. Qed.
 
 Lemma size_exp_leq p n : size (p ^+ n) <= ((size p).-1 * n).+1.
 Proof.
@@ -665,7 +663,7 @@ by case: leqP => // le_p_n; rewrite nth_default ?mulr0.
 Qed.
 
 Fact scale_polyA a b p : scale_poly a (scale_poly b p) = scale_poly (a * b) p.
-Proof. by rewrite !scale_polyE mulrA polyC_mul. Qed.
+Proof. by rewrite !scale_polyE mulrA polyCM. Qed.
 
 Fact scale_1poly : left_id 1 scale_poly.
 Proof. by move=> p; rewrite scale_polyE mul1r. Qed.
@@ -761,9 +759,7 @@ by elim: {p}(p : seq R) => //= p c IHp; rewrite cons_poly_def; apply: Kcons.
 Qed.
 
 Lemma polyseqXsubC a : 'X - a%:P = [:: - a; 1] :> seq R.
-Proof.
-by rewrite -['X]mul1r -polyC_opp -cons_poly_def polyseq_cons polyseq1.
-Qed.
+Proof. by rewrite -['X]mul1r -polyCN -cons_poly_def polyseq_cons polyseq1. Qed.
 
 Lemma size_XsubC a : size ('X - a%:P) = 2%N.
 Proof. by rewrite polyseqXsubC. Qed.
@@ -843,7 +839,7 @@ Lemma poly_def n E : \poly_(i < n) E i = \sum_(i < n) E i *: 'X^i.
 Proof.
 rewrite unlock; elim: n => [|n IHn] in E *; first by rewrite big_ord0.
 rewrite big_ord_recl /= cons_poly_def addrC expr0 alg_polyC.
-congr (_ + _); rewrite (iota_addl 1 0) -map_comp IHn big_distrl /=.
+congr (_ + _); rewrite (iotaDl 1 0) -map_comp IHn big_distrl /=.
 by apply: eq_bigr => i _; rewrite -scalerAl exprSr.
 Qed.
 
@@ -1065,7 +1061,7 @@ Proof. by elim/big_rec2: _ => [|i _ p _ <-]; rewrite (horner0, hornerD). Qed.
 Lemma hornerCM a p x : (a%:P * p).[x] = a * p.[x].
 Proof.
 elim/poly_ind: p => [|p c IHp]; first by rewrite !(mulr0, horner0).
-by rewrite mulrDr mulrA -polyC_mul !hornerMXaddC IHp mulrDr mulrA.
+by rewrite mulrDr mulrA -polyCM !hornerMXaddC IHp mulrDr mulrA.
 Qed.
 
 Lemma hornerZ c p x : (c *: p).[x] = c * p.[x].
@@ -1528,7 +1524,7 @@ Proof. by case: n => // n; rewrite derivSn derivC linear0. Qed.
 Lemma derivnD n : {morph derivn n : p q / p + q}.
 Proof. exact: linearD. Qed.
 
-Lemma derivn_sub n : {morph derivn n : p q / p - q}.
+Lemma derivnB n : {morph derivn n : p q / p - q}.
 Proof. exact: linearB. Qed.
 
 Lemma derivnMn n m p : (p *+ m)^`(n) = p^`(n) *+ m.
@@ -2219,7 +2215,7 @@ Definition poly_inv p := if p \in poly_unit then (p`_0)^-1%:P else p.
 Fact poly_mulVp : {in poly_unit, left_inverse 1 poly_inv *%R}.
 Proof.
 move=> p Up; rewrite /poly_inv Up.
-by case/andP: Up => /size_poly1P[c _ ->]; rewrite coefC -polyC_mul => /mulVr->.
+by case/andP: Up => /size_poly1P[c _ ->]; rewrite coefC -polyCM => /mulVr->.
 Qed.
 
 Fact poly_intro_unit p q : q * p = 1 -> p \in poly_unit.
@@ -2264,7 +2260,7 @@ Proof. by []. Qed.
 Lemma poly_invE p : p ^-1 = if p \in GRing.unit then (p`_0)^-1%:P else p.
 Proof. by []. Qed.
 
-Lemma polyC_inv c : c%:P^-1 = (c^-1)%:P.
+Lemma polyCV c : c%:P^-1 = (c^-1)%:P.
 Proof.
 have [/rmorphV-> // | nUc] := boolP (c \in GRing.unit).
 by rewrite !invr_out // poly_unitE coefC (negbTE nUc) andbF.
@@ -2771,3 +2767,31 @@ by rewrite monic_prod => // i; rewrite monicXsubC.
 Qed.
 
 End ClosedField.
+
+Notation "@ 'polyC_add'" :=
+  (deprecate polyC_add polyCD) (at level 10, only parsing) : fun_scope.
+Notation "@ 'polyC_opp'" :=
+  (deprecate polyC_opp polyCN) (at level 10, only parsing) : fun_scope.
+Notation "@ 'polyC_sub'" :=
+  (deprecate polyC_sub polyCB) (at level 10, only parsing) : fun_scope.
+Notation "@ 'polyC_muln'" :=
+  (deprecate polyC_muln polyCMn) (at level 10, only parsing) : fun_scope.
+Notation "@ 'polyC_mul'" :=
+  (deprecate polyC_mul polyCM) (at level 10, only parsing) : fun_scope.
+Notation "@ 'polyC_exp'" :=
+  (deprecate polyC_exp polyCX) (at level 10, only parsing) : fun_scope.
+Notation "@ 'polyC_inv'" :=
+  (deprecate polyC_inv polyCV) (at level 10, only parsing) : fun_scope.
+Notation "@ 'lead_coef_opp'" :=
+  (deprecate lead_coef_opp lead_coefN) (at level 10, only parsing) : fun_scope.
+Notation "@ 'derivn_sub'" :=
+  (deprecate derivn_sub derivnB) (at level 10, only parsing) : fun_scope.
+Notation polyC_add := (@polyC_add _) (only parsing).
+Notation polyC_opp := (@polyC_opp _) (only parsing).
+Notation polyC_sub := (@polyC_sub _) (only parsing).
+Notation polyC_muln := (@polyC_muln _) (only parsing).
+Notation polyC_mul := (@polyC_mul _) (only parsing).
+Notation polyC_exp := (@polyC_exp _) (only parsing).
+Notation polyC_inv := (@polyC_inv _) (only parsing).
+Notation lead_coef_opp := (@lead_coef_opp _) (only parsing).
+Notation derivn_sub := (@derivn_sub _) (only parsing).
diff --git a/mathcomp/algebra/polyXY.v b/mathcomp/algebra/polyXY.v
index 9bc8fd5..5a84da7 100644
--- a/mathcomp/algebra/polyXY.v
+++ b/mathcomp/algebra/polyXY.v
@@ -136,7 +136,7 @@ Qed.
 Lemma max_size_evalC u x : size u.[x%:P] <= sizeY u.
 Proof.
 rewrite horner_coef (leq_trans (size_sum _ _ _)) //; apply/bigmax_leqP=> i _.
-rewrite (leq_trans (size_mul_leq _ _)) // -polyC_exp size_polyC addnC -subn1.
+rewrite (leq_trans (size_mul_leq _ _)) // -polyCX size_polyC addnC -subn1.
 by rewrite (leq_trans _ (max_size_coefXY _ i)) // leq_subLR leq_add2r leq_b1.
 Qed.
 
@@ -192,7 +192,7 @@ Lemma horner_swapXY u x : (swapXY u).[x%:P] = u ^ eval x.
 Proof.
 apply/polyP=> i /=; rewrite coef_map /= /eval horner_coef coef_sum -sizeYE.
 rewrite (horner_coef_wide _ (max_size_coefXY u i)); apply: eq_bigr=> j _.
-by rewrite -polyC_exp coefMC coef_swapXY.
+by rewrite -polyCX coefMC coef_swapXY.
 Qed.
 
 Lemma horner_polyC u x : u.[x%:P] = swapXY u ^ eval x.
@@ -228,7 +228,7 @@ Proof. by rewrite -!size_poly_eq0 size_poly_XmY. Qed.
 
 Lemma lead_coef_poly_XaY p : lead_coef (poly_XaY p) = (lead_coef p)%:P.
 Proof.
-rewrite lead_coef_comp ?size_XaddC // -['Y]opprK -polyC_opp lead_coefXsubC.
+rewrite lead_coef_comp ?size_XaddC // -['Y]opprK -polyCN lead_coefXsubC.
 by rewrite expr1n mulr1 lead_coef_map_inj //; apply: polyC_inj.
 Qed.
 
diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v
index a7d3b1e..ebb8a5b 100644
--- a/mathcomp/algebra/polydiv.v
+++ b/mathcomp/algebra/polydiv.v
@@ -365,7 +365,7 @@ elim: (size m) 0%N 0 {1 4 6}m (leqnn (size m)) => [|n IHn] k q r Hr /=.
   by rewrite size_poly0 size_poly_gt0.
 case: ltnP => Hlt Heq; first by constructor.
 apply/IHn=> [|Cda]; last first.
-  rewrite mulrDl addrAC -addrA subrK exprSr polyC_mul mulrA Heq //.
+  rewrite mulrDl addrAC -addrA subrK exprSr polyCM mulrA Heq //.
   by rewrite mulrDl -mulrA Cda mulrA.
 apply/leq_sizeP => j Hj; rewrite coefB coefMC -scalerAl coefZ coefXnM.
 rewrite ltn_subRL ltnNge (leq_trans Hr) /=; last first.
@@ -427,7 +427,7 @@ move=> lt_rd; case: comm_redivpP=> k q1 r1 /(_ Cdl) Heq.
 have dn0: d != 0 by case: (size d) lt_rd (size_poly_eq0 d) => // n _ <-.
 move=> /(_ dn0) Hs.
 have eC : q * d * (lead_coef d ^+ k)%:P = q * (lead_coef d ^+ k)%:P * d.
-  by rewrite -mulrA polyC_exp (commrX k Cdl) mulrA.
+  by rewrite -mulrA polyCX (commrX k Cdl) mulrA.
 suff e1 : q1 = q * (lead_coef d ^+ k)%:P.
   congr (_, _, _) => //=; move/eqP: Heq.
   by rewrite [_ + r1]addrC -subr_eq e1 mulrDl addrAC eC subrr add0r; move/eqP.
@@ -463,9 +463,9 @@ suff:
   (rmodp p d) * (lq ^+ (m - v))%:P == 0.
   rewrite rreg_div0 //; first by case/andP.
   by rewrite rreg_size ?ltn_rmodp //; exact: rregX.
-rewrite mulrDl addrAC mulNr -!mulrA polyC_exp -(commrX (m-v) Cdl).
-rewrite -polyC_exp mulrA -mulrDl -rdivp_eq // [(_ ^+ (m - k))%:P]polyC_exp.
-rewrite -(commrX (m-k) Cdl) -polyC_exp mulrA -he -!mulrA -!polyC_mul -/v.
+rewrite mulrDl addrAC mulNr -!mulrA polyCX -(commrX (m-v) Cdl).
+rewrite -polyCX mulrA -mulrDl -rdivp_eq // [(_ ^+ (m - k))%:P]polyCX.
+rewrite -(commrX (m-k) Cdl) -polyCX mulrA -he -!mulrA -!polyCM -/v.
 by rewrite -!exprD addnC subnK ?leq_maxl // addnC subnK ?subrr ?leq_maxr.
 Qed.
 
@@ -495,7 +495,7 @@ Proof.
 have dn0 : d != 0 by rewrite -lead_coef_eq0 rreg_neq0.
 move: (rdivp_eq d); rewrite rmodpp addr0.
 suff ->: GRing.comm d (lead_coef d ^+ rscalp d d)%:P by move/(rreg_lead Rreg)->.
-by rewrite polyC_exp; apply: commrX.
+by rewrite polyCX; apply: commrX.
 Qed.
 
 Lemma rdvdpp : rdvdp d d. Proof. exact/eqP/rmodpp. Qed.
@@ -553,15 +553,15 @@ case: (monic_comreg mond)=> Hc Hr; rewrite [r in _ * _ + r]rdivp_eq addrA.
 by rewrite -mulrDl rdivp_addl_mul_small // ltn_rmodp monic_neq0.
 Qed.
 
-Lemma rdivp_addl q r : rdvdp d q -> rdivp (q + r) d = rdivp q d + rdivp r d.
+Lemma rdivpDl q r : rdvdp d q -> rdivp (q + r) d = rdivp q d + rdivp r d.
 Proof.
 case: (monic_comreg mond)=> Hc Hr; rewrite [r in q + r]rdivp_eq addrA.
 rewrite [q in q + _ + _]rdivp_eq; move/rmodp_eq0P->.
 by rewrite addr0 -mulrDl rdivp_addl_mul_small // ltn_rmodp monic_neq0.
 Qed.
 
-Lemma rdivp_addr q r : rdvdp d r -> rdivp (q + r) d = rdivp q d + rdivp r d.
-Proof. by rewrite addrC; move/rdivp_addl->; rewrite addrC. Qed.
+Lemma rdivpDr q r : rdvdp d r -> rdivp (q + r) d = rdivp q d + rdivp r d.
+Proof. by rewrite addrC; move/rdivpDl->; rewrite addrC. Qed.
 
 Lemma rdivp_mull p : rdivp (p * d) d = p.
 Proof. by rewrite -[p * d]addr0 rdivp_addl_mul rdiv0p addr0. Qed.
@@ -581,7 +581,7 @@ Proof.
 by move=> Hd; case: (monic_comreg mond)=> Hc Hr; rewrite /rmodp redivp_eq.
 Qed.
 
-Lemma rmodp_add p q : rmodp (p + q) d = rmodp p d + rmodp q d.
+Lemma rmodpD p q : rmodp (p + q) d = rmodp p d + rmodp q d.
 Proof.
 rewrite [p in LHS]rdivp_eq [q in LHS]rdivp_eq addrACA -mulrDl.
 rewrite rmodp_addl_mul_small //; apply: (leq_ltn_trans (size_add _ _)).
@@ -590,7 +590,7 @@ Qed.
 
 Lemma rmodp_mulmr p q : rmodp (p * (rmodp q d)) d = rmodp (p * q) d.
 Proof.
-by rewrite [q in RHS]rdivp_eq mulrDr rmodp_add mulrA rmodp_mull add0r.
+by rewrite [q in RHS]rdivp_eq mulrDr rmodpD mulrA rmodp_mull add0r.
 Qed.
 
 Lemma rdvdpp : rdvdp d d.
@@ -623,6 +623,19 @@ Lemma rdivpK p : rdvdp d p -> (rdivp p d) * d = p.
 Proof. by move=> dvddp; rewrite [RHS]rdivp_eq rmodp_eq0 ?addr0. Qed.
 
 End MonicDivisor.
+
+Notation "@ 'rdivp_addl'" :=
+  (deprecate rdivp_addl rdivpDl) (at level 10, only parsing) : fun_scope.
+Notation "@ 'rdivp_addr'" :=
+  (deprecate rdivp_addr rdivpDr) (at level 10, only parsing) : fun_scope.
+Notation "@ 'rmodp_add'" :=
+  (deprecate rmodp_add rmodpD) (at level 10, only parsing) : fun_scope.
+Notation rdivp_addl :=
+  (fun d_monic => @rdivp_addl _ _ d_monic _) (only parsing).
+Notation rdivp_addr :=
+  (fun d_monic q => @rdivp_addr _ _ d_monic q _) (only parsing).
+Notation rmodp_add := (@rmodp_add _ _) (only parsing).
+
 End RingMonic.
 
 Module Ring.
@@ -824,8 +837,8 @@ rewrite unlock ud redivp_def; constructor => //.
   rewrite -scalerAl -scalerDr -mul_polyC.
   have hn0 : (lead_coef d ^+ rscalp m d)%:P != 0.
     by rewrite polyC_eq0; apply: expf_neq0.
-  apply: (mulfI hn0); rewrite !mulrA -exprVn !polyC_exp -exprMn -polyC_mul.
-  by rewrite divrr // expr1n mul1r -polyC_exp mul_polyC rdivp_eq.
+  apply: (mulfI hn0); rewrite !mulrA -exprVn !polyCX -exprMn -polyCM.
+  by rewrite divrr // expr1n mul1r -polyCX mul_polyC rdivp_eq.
 move=> dn0; rewrite size_scale ?ltn_rmodp // -exprVn expf_eq0 negb_and.
 by rewrite invr_eq0 cdn0 orbT.
 Qed.
@@ -1415,13 +1428,13 @@ suff Hmn m n: m %= n -> (m %| p) -> (n %| p).
 by rewrite /eqp; case/andP=> dd' d'd dp; apply: (dvdp_trans d'd).
 Qed.
 
-Lemma dvdp_scaler c m n : c != 0 -> m %| c *: n = (m %| n).
+Lemma dvdpZr c m n : c != 0 -> m %| c *: n = (m %| n).
 Proof. by move=> cn0; exact/eqp_dvdr/eqp_scale. Qed.
 
-Lemma dvdp_scalel c m n : c != 0 -> (c *: m %| n) = (m %| n).
+Lemma dvdpZl c m n : c != 0 -> (c *: m %| n) = (m %| n).
 Proof. by move=> cn0; exact/eqp_dvdl/eqp_scale. Qed.
 
-Lemma dvdp_opp d p : d %| (- p) = (d %| p).
+Lemma dvdpN d p : d %| (- p) = (d %| p).
 Proof. by apply: eqp_dvdr; rewrite -scaleN1r eqp_scale ?oppr_eq0 ?oner_eq0. Qed.
 
 Lemma eqp_mul2r r p q : r != 0 -> (p * r %= q * r) = (p %= q).
@@ -1660,7 +1673,7 @@ rewrite (polySpred mn0) addSn /= -[n in _ <= n]add0n leq_add2r -ltnS.
 rewrite -polySpred //= leq_eqVlt ltnS size_poly_leq0 (negPf mn0) orbF.
 case/size_poly1P=> c cn0 -> {mn0 m}; rewrite mul_polyC.
 suff -> : n %% (c *: n) = 0 by rewrite gcd0p; apply: eqp_scale.
-by apply/modp_eq0P; rewrite dvdp_scalel.
+by apply/modp_eq0P; rewrite dvdpZl.
 Qed.
 
 Lemma gcdp_mulr m n : gcdp n (n * m) %= n.
@@ -1670,8 +1683,8 @@ Lemma gcdp_scalel c m n : c != 0 -> gcdp (c *: m) n %= gcdp m n.
 Proof.
 move=> cn0; rewrite /eqp dvdp_gcd [gcdp m n %| _]dvdp_gcd !dvdp_gcdr !andbT.
 apply/andP; split; last first.
-  by apply: dvdp_trans (dvdp_gcdl _ _) _; rewrite dvdp_scaler.
-by apply: dvdp_trans (dvdp_gcdl _ _) _; rewrite dvdp_scalel.
+  by apply: dvdp_trans (dvdp_gcdl _ _) _; rewrite dvdpZr.
+by apply: dvdp_trans (dvdp_gcdl _ _) _; rewrite dvdpZl.
 Qed.
 
 Lemma gcdp_scaler c m n : c != 0 -> gcdp m (c *: n) %= gcdp m n.
@@ -1764,10 +1777,10 @@ Proof. by rewrite /coprimep=> /eqP. Qed.
 Lemma coprimep_def p q : coprimep p q = (size (gcdp p q) == 1%N).
 Proof. done. Qed.
 
-Lemma coprimep_scalel c m n : c != 0 -> coprimep (c *: m) n = coprimep m n.
+Lemma coprimepZl c m n : c != 0 -> coprimep (c *: m) n = coprimep m n.
 Proof. by move=> ?; rewrite !coprimep_def (eqp_size (gcdp_scalel _ _ _)). Qed.
 
-Lemma coprimep_scaler c m n: c != 0 -> coprimep m (c *: n) = coprimep m n.
+Lemma coprimepZr c m n: c != 0 -> coprimep m (c *: n) = coprimep m n.
 Proof. by move=> ?; rewrite !coprimep_def (eqp_size (gcdp_scaler _ _ _)). Qed.
 
 Lemma coprimepp p : coprimep p p = (size p == 1%N).
@@ -1981,7 +1994,7 @@ Qed.
 Lemma Gauss_gcdpl p m n : coprimep p n -> gcdp p (m * n) %= gcdp p m.
 Proof. by move=> co_pn; rewrite mulrC Gauss_gcdpr. Qed.
 
-Lemma coprimep_mulr p q r : coprimep p (q * r) = (coprimep p q && coprimep p r).
+Lemma coprimepMr p q r : coprimep p (q * r) = (coprimep p q && coprimep p r).
 Proof.
 apply/coprimepP/andP=> [hp | [/coprimepP-hq hr]].
   by split; apply/coprimepP=> d dp dq; rewrite hp //;
@@ -1991,8 +2004,8 @@ rewrite Gauss_dvdpl in dqr; first exact: hq.
 by move/coprimep_dvdr: hr; apply.
 Qed.
 
-Lemma coprimep_mull p q r: coprimep (q * r) p = (coprimep q p && coprimep r p).
-Proof. by rewrite ![coprimep _ p]coprimep_sym coprimep_mulr. Qed.
+Lemma coprimepMl p q r: coprimep (q * r) p = (coprimep q p && coprimep r p).
+Proof. by rewrite ![coprimep _ p]coprimep_sym coprimepMr. Qed.
 
 Lemma modp_coprime k u n : k != 0 -> (k * u) %% n %= 1 -> coprimep k n.
 Proof.
@@ -2005,17 +2018,17 @@ Qed.
 Lemma coprimep_pexpl k m n : 0 < k -> coprimep (m ^+ k) n = coprimep m n.
 Proof.
 case: k => // k _; elim: k => [|k IHk]; first by rewrite expr1.
-by rewrite exprS coprimep_mull -IHk andbb.
+by rewrite exprS coprimepMl -IHk andbb.
 Qed.
 
 Lemma coprimep_pexpr k m n : 0 < k -> coprimep m (n ^+ k) = coprimep m n.
 Proof. by move=> k_gt0; rewrite !(coprimep_sym m) coprimep_pexpl. Qed.
 
-Lemma coprimep_expl k m n : coprimep m n -> coprimep (m ^+ k) n.
+Lemma coprimepXl k m n : coprimep m n -> coprimep (m ^+ k) n.
 Proof. by case: k => [|k] co_pm; rewrite ?coprime1p // coprimep_pexpl. Qed.
 
-Lemma coprimep_expr k m n : coprimep m n -> coprimep m (n ^+ k).
-Proof. by rewrite !(coprimep_sym m); apply: coprimep_expl. Qed.
+Lemma coprimepXr k m n : coprimep m n -> coprimep m (n ^+ k).
+Proof. by rewrite !(coprimep_sym m); apply: coprimepXl. Qed.
 
 Lemma gcdp_mul2l p q r : gcdp (p * q) (p * r) %= (p * gcdp q r).
 Proof.
@@ -2108,8 +2121,8 @@ have dn0 : d != 0 by rewrite gcdp_eq0 negb_and nn0 orbT.
 have c1n0 : c1 != 0 by rewrite !expf_neq0 // lead_coef_eq0.
 have c2n0 : c2 != 0 by rewrite !expf_neq0 // lead_coef_eq0.
 have c2k_n0 : c2 ^+ k != 0 by rewrite !expf_neq0 // lead_coef_eq0.
-rewrite -(@dvdp_scaler (c1 ^+ k)) ?expf_neq0 ?lead_coef_eq0 //.
-rewrite -(@dvdp_scalel (c2 ^+ k)) // -!exprZn def_m def_n !exprMn.
+rewrite -(@dvdpZr (c1 ^+ k)) ?expf_neq0 ?lead_coef_eq0 //.
+rewrite -(@dvdpZl (c2 ^+ k)) // -!exprZn def_m def_n !exprMn.
 rewrite dvdp_mul2r ?expf_neq0 //.
 have: coprimep (m' ^+ k) (n' ^+ k).
   by rewrite coprimep_pexpl // coprimep_pexpr // coprimep_div_gcd ?mn0.
@@ -2120,8 +2133,8 @@ have /size_poly1P [c cn0 em'] : size m' == 1%N.
   have := hc _ (dvdpp _) hd; rewrite -size_poly_eq1.
   rewrite polySpred; last by rewrite expf_eq0 negb_and m'_n0 orbT.
   by rewrite size_exp eqSS muln_eq0 orbC eqn0Ngt k_gt0 /= -eqSS -polySpred.
-rewrite -(@dvdp_scalel c2) // def_m em' mul_polyC dvdp_scalel //.
-by rewrite -(@dvdp_scaler c1) // def_n dvdp_mull.
+rewrite -(@dvdpZl c2) // def_m em' mul_polyC dvdpZl //.
+by rewrite -(@dvdpZr c1) // def_n dvdp_mull.
 Qed.
 
 Lemma root_gcd p q x : root (gcdp p q) x = root p x && root q x.
@@ -2285,7 +2298,7 @@ Qed.
 Lemma coprimep_XsubC p c : coprimep p ('X - c%:P) = ~~ root p c.
 Proof.
 rewrite -coprimep_modl modp_XsubC /root -alg_polyC.
-have [-> | /coprimep_scalel->] := eqVneq; last exact: coprime1p.
+have [-> | /coprimepZl->] := eqVneq; last exact: coprime1p.
 by rewrite scale0r /coprimep gcd0p size_XsubC.
 Qed.
 
@@ -2340,6 +2353,34 @@ End IDomainPseudoDivision.
 Hint Resolve eqpxx divp0 divp1 mod0p modp0 modp1 dvdp_mull dvdp_mulr dvdpp : core.
 Hint Resolve dvdp0 : core.
 
+Notation "@ 'dvdp_scalel'" :=
+  (deprecate dvdp_scalel dvdpZl) (at level 10, only parsing) : fun_scope.
+Notation "@ 'dvdp_scaler'" :=
+  (deprecate dvdp_scaler dvdpZr) (at level 10, only parsing) : fun_scope.
+Notation "@ 'dvdp_opp'" :=
+  (deprecate dvdp_opp dvdpN) (at level 10, only parsing) : fun_scope.
+Notation "@ 'coprimep_scalel'" :=
+  (deprecate coprimep_scalel coprimepZl) (at level 10, only parsing) : fun_scope.
+Notation "@ 'coprimep_scaler'" :=
+  (deprecate coprimep_scaler coprimepZr) (at level 10, only parsing) : fun_scope.
+Notation "@ 'coprimep_mull'" :=
+  (deprecate coprimep_mull coprimepMl) (at level 10, only parsing) : fun_scope.
+Notation "@ 'coprimep_mulr'" :=
+  (deprecate coprimep_mulr coprimepMr) (at level 10, only parsing) : fun_scope.
+Notation "@ 'coprimep_expl'" :=
+  (deprecate coprimep_expl coprimepXl) (at level 10, only parsing) : fun_scope.
+Notation "@ 'coprimep_expr'" :=
+  (deprecate coprimep_expr coprimepXr) (at level 10, only parsing) : fun_scope.
+Notation dvdp_scalel := (@dvdp_scalel _ _) (only parsing).
+Notation dvdp_scaler := (@dvdp_scaler _ _) (only parsing).
+Notation dvdp_opp := (@dvdp_opp _) (only parsing).
+Notation coprimep_scalel := (@coprimep_scalel _ _) (only parsing).
+Notation coprimep_scaler := (@coprimep_scaler _ _) (only parsing).
+Notation coprimep_mull := (@coprimep_mull _) (only parsing).
+Notation coprimep_mulr := (@coprimep_mulr _) (only parsing).
+Notation coprimep_expl := (fun k => @coprimep_expl _ k _ _) (only parsing).
+Notation coprimep_expr := (fun k => @coprimep_expr _ k _ _) (only parsing).
+
 End CommonIdomain.
 
 Module Idomain.
@@ -2461,7 +2502,7 @@ move=> ulcq /eqp_eq; move/(congr1 ( *:%R (lead_coef q)^-1 )).
 by rewrite !scalerA mulrC divrr // scale1r mulrC.
 Qed.
 
-Lemma modp_scalel c p : (c *: p) %% d = c *: (p %% d).
+Lemma modpZl c p : (c *: p) %% d = c *: (p %% d).
 Proof.
 have [-> | cn0] := eqVneq c 0; first by rewrite !scale0r mod0p.
 have e : (c *: p) = (c *: (p %/ d)) * d + c *: (p %% d).
@@ -2472,7 +2513,7 @@ rewrite size_polyC cn0 addSn add0n /= ltn_modp -lead_coef_eq0.
 by apply: contraTneq ulcd => ->; rewrite unitr0.
 Qed.
 
-Lemma divp_scalel c p : (c *: p) %/ d = c *: (p %/ d).
+Lemma divpZl c p : (c *: p) %/ d = c *: (p %/ d).
 Proof.
 have [-> | cn0] := eqVneq c 0; first by rewrite !scale0r div0p.
 have e : (c *: p) = (c *: (p %/ d)) * d + c *: (p %% d).
@@ -2486,22 +2527,22 @@ Qed.
 Lemma eqp_modpl p q : p %= q -> (p %% d) %= (q %% d).
 Proof.
 case/eqpP=> [[c1 c2]] /andP /= [c1n0 c2n0 e].
-by apply/eqpP; exists (c1, c2); rewrite ?c1n0 //= -!modp_scalel e.
+by apply/eqpP; exists (c1, c2); rewrite ?c1n0 //= -!modpZl e.
 Qed.
 
 Lemma eqp_divl p q : p %= q -> (p %/ d) %= (q %/ d).
 Proof.
 case/eqpP=> [[c1 c2]] /andP /= [c1n0 c2n0 e].
-by apply/eqpP; exists (c1, c2); rewrite ?c1n0 // -!divp_scalel e.
+by apply/eqpP; exists (c1, c2); rewrite ?c1n0 // -!divpZl e.
 Qed.
 
-Lemma modp_opp p : (- p) %% d = - (p %% d).
-Proof. by rewrite -mulN1r -[RHS]mulN1r -polyC_opp !mul_polyC modp_scalel. Qed.
+Lemma modpN p : (- p) %% d = - (p %% d).
+Proof. by rewrite -mulN1r -[RHS]mulN1r -polyCN !mul_polyC modpZl. Qed.
 
-Lemma divp_opp p : (- p) %/ d = - (p %/ d).
-Proof. by rewrite -mulN1r -[RHS]mulN1r -polyC_opp !mul_polyC divp_scalel. Qed.
+Lemma divpN p : (- p) %/ d = - (p %/ d).
+Proof. by rewrite -mulN1r -[RHS]mulN1r -polyCN !mul_polyC divpZl. Qed.
 
-Lemma modp_add p q : (p + q) %% d = p %% d + q %% d.
+Lemma modpD p q : (p + q) %% d = p %% d + q %% d.
 Proof.
 have/edivpP [] // : (p + q) = (p %/ d + q %/ d) * d + (p %% d + q %% d).
   by rewrite mulrDl addrACA -!divp_eq.
@@ -2510,7 +2551,7 @@ rewrite gtn_max !ltn_modp andbb -lead_coef_eq0.
 by apply: contraTneq ulcd => ->; rewrite unitr0.
 Qed.
 
-Lemma divp_add p q : (p + q) %/ d = p %/ d + q %/ d.
+Lemma divpD p q : (p + q) %/ d = p %/ d + q %/ d.
 Proof.
 have/edivpP [] // : (p + q) = (p %/ d + q %/ d) * d + (p %% d + q %% d).
   by rewrite mulrDl addrACA -!divp_eq.
@@ -2527,16 +2568,14 @@ Qed.
 
 Lemma mulKp q : (d * q) %/ d = q. Proof. by rewrite mulrC; apply: mulpK. Qed.
 
-Lemma divp_addl_mul_small q r :
-  size r < size d -> (q * d + r) %/ d = q.
-Proof. by move=> srd; rewrite divp_add (divp_small srd) addr0 mulpK. Qed.
+Lemma divp_addl_mul_small q r : size r < size d -> (q * d + r) %/ d = q.
+Proof. by move=> srd; rewrite divpD (divp_small srd) addr0 mulpK. Qed.
 
-Lemma modp_addl_mul_small q r :
-  size r < size d -> (q * d + r) %% d = r.
-Proof. by move=> srd; rewrite modp_add modp_mull add0r modp_small. Qed.
+Lemma modp_addl_mul_small q r : size r < size d -> (q * d + r) %% d = r.
+Proof. by move=> srd; rewrite modpD modp_mull add0r modp_small. Qed.
 
 Lemma divp_addl_mul q r : (q * d + r) %/ d = q + r %/ d.
-Proof. by rewrite divp_add mulpK. Qed.
+Proof. by rewrite divpD mulpK. Qed.
 
 Lemma divpp : d %/ d = 1. Proof. by rewrite -[d in d %/ _]mul1r mulpK. Qed.
 
@@ -2584,7 +2623,7 @@ Lemma divp_mulCA p q : d %| p -> d %| q -> p * (q %/ d) = q * (p %/ d).
 Proof. by move=> hdp hdq; rewrite mulrC divp_mulAC // divp_mulA. Qed.
 
 Lemma modp_mul p q : (p * (q %% d)) %% d = (p * q) %% d.
-Proof. by rewrite [q in RHS]divp_eq mulrDr modp_add mulrA modp_mull add0r. Qed.
+Proof. by rewrite [q in RHS]divp_eq mulrDr modpD mulrA modp_mull add0r. Qed.
 
 End UnitDivisor.
 
@@ -2644,7 +2683,7 @@ Qed.
 Lemma divpAC p q : lead_coef p \in GRing.unit -> q %/ d %/ p = q %/ p %/ d.
 Proof. by move=> ulcp; rewrite !divp_divl // mulrC. Qed.
 
-Lemma modp_scaler c p : c \in GRing.unit -> p %% (c *: d) = (p %% d).
+Lemma modpZr c p : c \in GRing.unit -> p %% (c *: d) = (p %% d).
 Proof.
 case: (eqVneq d 0) => [-> | dn0 cn0]; first by rewrite scaler0 !modp0.
 have e : p = (c^-1 *: (p %/ d)) * (c *: d) + (p %% d).
@@ -2654,7 +2693,7 @@ suff s : size (p %% d) < size (c *: d).
 by rewrite size_scale ?ltn_modp //; apply: contraTneq cn0 => ->; rewrite unitr0.
 Qed.
 
-Lemma divp_scaler c p : c \in GRing.unit -> p %/ (c *: d) = c^-1 *: (p %/ d).
+Lemma divpZr c p : c \in GRing.unit -> p %/ (c *: d) = c^-1 *: (p %/ d).
 Proof.
 case: (eqVneq d 0) => [-> | dn0 cn0]; first by rewrite scaler0 !divp0 scaler0.
 have e : p = (c^-1 *: (p %/ d)) * (c *: d) + (p %% d).
@@ -2666,6 +2705,31 @@ Qed.
 
 End MoreUnitDivisor.
 
+Notation "@ 'modp_scalel'" :=
+  (deprecate modp_scalel modpZl) (at level 10, only parsing) : fun_scope.
+Notation "@ 'modp_scaler'" :=
+  (deprecate modp_scaler modpZr) (at level 10, only parsing) : fun_scope.
+Notation "@ 'modp_opp'" :=
+  (deprecate modp_opp modpN) (at level 10, only parsing) : fun_scope.
+Notation "@ 'modp_add'" :=
+  (deprecate modp_add modpD) (at level 10, only parsing) : fun_scope.
+Notation "@ 'divp_scalel'" :=
+  (deprecate divp_scalel divpZl) (at level 10, only parsing) : fun_scope.
+Notation "@ 'divp_scaler'" :=
+  (deprecate divp_scaler divpZr) (at level 10, only parsing) : fun_scope.
+Notation "@ 'divp_opp'" :=
+  (deprecate divp_opp divpN) (at level 10, only parsing) : fun_scope.
+Notation "@ 'divp_add'" :=
+  (deprecate divp_add divpD) (at level 10, only parsing) : fun_scope.
+Notation modp_scalel := (@modp_scalel _ _) (only parsing).
+Notation modp_scaler := (fun d_unit => @modp_scaler _ _ d_unit _) (only parsing).
+Notation modp_opp := (@modp_opp _ _) (only parsing).
+Notation modp_add := (@modp_add _ _) (only parsing).
+Notation divp_scalel := (@divp_scalel _ _) (only parsing).
+Notation divp_scaler := (fun d_unit => @divp_scaler _ _ d_unit _) (only parsing).
+Notation divp_opp := (@divp_opp _ _) (only parsing).
+Notation divp_add := (@divp_add _ _) (only parsing).
+
 End IdomainUnit.
 
 Module Field.
@@ -2724,10 +2788,10 @@ case/IdomainUnit.ulc_eqpP; first by rewrite unitfE lead_coef_eq0.
 by move=> c nz_c ->; exists c.
 Qed.
 
-Lemma modp_scalel c p q : (c *: p) %% q = c *: (p %% q).
+Lemma modpZl c p q : (c *: p) %% q = c *: (p %% q).
 Proof.
 have [-> | qn0] := eqVneq q 0; first by rewrite !modp0.
-by apply: IdomainUnit.modp_scalel; rewrite unitfE lead_coef_eq0.
+by apply: IdomainUnit.modpZl; rewrite unitfE lead_coef_eq0.
 Qed.
 
 Lemma mulpK p q : q != 0 -> p * q %/ q = p.
@@ -2736,13 +2800,13 @@ Proof. by move=> qn0; rewrite IdomainUnit.mulpK // unitfE lead_coef_eq0. Qed.
 Lemma mulKp p q : q != 0 -> q * p %/ q = p.
 Proof. by rewrite mulrC; apply: mulpK. Qed.
 
-Lemma divp_scalel c p q : (c *: p) %/ q = c *: (p %/ q).
+Lemma divpZl c p q : (c *: p) %/ q = c *: (p %/ q).
 Proof.
 have [-> | qn0] := eqVneq q 0; first by rewrite !divp0 scaler0.
-by apply: IdomainUnit.divp_scalel; rewrite unitfE lead_coef_eq0.
+by apply: IdomainUnit.divpZl; rewrite unitfE lead_coef_eq0.
 Qed.
 
-Lemma modp_scaler c p d : c != 0 -> p %% (c *: d) = (p %% d).
+Lemma modpZr c p d : c != 0 -> p %% (c *: d) = (p %% d).
 Proof.
 case: (eqVneq d 0) => [-> | dn0 cn0]; first by rewrite scaler0 !modp0.
 have e : p = (c^-1 *: (p %/ d)) * (c *: d) + (p %% d).
@@ -2751,7 +2815,7 @@ suff s : size (p %% d) < size (c *: d) by rewrite (modpP e s).
 by rewrite size_scale ?ltn_modp.
 Qed.
 
-Lemma divp_scaler c p d : c != 0 -> p %/ (c *: d) = c^-1 *: (p %/ d).
+Lemma divpZr c p d : c != 0 -> p %/ (c *: d) = c^-1 *: (p %/ d).
 Proof.
 case: (eqVneq d 0) => [-> | dn0 cn0]; first by rewrite scaler0 !divp0 scaler0.
 have e : p = (c^-1 *: (p %/ d)) * (c *: d) + (p %% d).
@@ -2763,20 +2827,20 @@ Qed.
 Lemma eqp_modpl d p q : p %= q -> (p %% d) %= (q %% d).
 Proof.
 case/eqpP=> [[c1 c2]] /andP /= [c1n0 c2n0 e].
-by apply/eqpP; exists (c1, c2); rewrite ?c1n0 // -!modp_scalel e.
+by apply/eqpP; exists (c1, c2); rewrite ?c1n0 // -!modpZl e.
 Qed.
 
 Lemma eqp_divl d p q : p %= q -> (p %/ d) %= (q %/ d).
 Proof.
 case/eqpP=> [[c1 c2]] /andP /= [c1n0 c2n0 e].
-by apply/eqpP; exists (c1, c2); rewrite ?c1n0 // -!divp_scalel e.
+by apply/eqpP; exists (c1, c2); rewrite ?c1n0 // -!divpZl e.
 Qed.
 
 Lemma eqp_modpr d p q : p %= q -> (d %% p) %= (d %% q).
 Proof.
 case/eqpP=> [[c1 c2]] /andP [c1n0 c2n0 e].
 have -> : p = (c1^-1 * c2) *: q by rewrite -scalerA -e scalerA mulVf // scale1r.
-by rewrite modp_scaler ?eqpxx // mulf_eq0 negb_or invr_eq0 c1n0.
+by rewrite modpZr ?eqpxx // mulf_eq0 negb_or invr_eq0 c1n0.
 Qed.
 
 Lemma eqp_mod p1 p2 q1 q2 : p1 %= p2 -> q1 %= q2 -> p1 %% q1 %= p2 %% q2.
@@ -2786,7 +2850,7 @@ Lemma eqp_divr (d m n : {poly F}) : m %= n -> (d %/ m) %= (d %/ n).
 Proof.
 case/eqpP=> [[c1 c2]] /andP [c1n0 c2n0 e].
 have -> : m = (c1^-1 * c2) *: n by rewrite -scalerA -e scalerA mulVf // scale1r.
-by rewrite divp_scaler ?eqp_scale // ?invr_eq0 mulf_eq0 negb_or invr_eq0 c1n0.
+by rewrite divpZr ?eqp_scale // ?invr_eq0 mulf_eq0 negb_or invr_eq0 c1n0.
 Qed.
 
 Lemma eqp_div p1 p2 q1 q2 : p1 %= p2 -> q1 %= q2 -> p1 %/ q1 %= p2 %/ q2.
@@ -2823,37 +2887,37 @@ case: ifP=> // _; apply: ihn => //; apply: eqp_trans (eqp_rdiv_div _ _) _.
 by apply: eqp_div => //; apply: eqp_trans (eqp_rgcd_gcd _ _) _; apply: eqp_gcd.
 Qed.
 
-Lemma modp_add d p q : (p + q) %% d = p %% d + q %% d.
+Lemma modpD d p q : (p + q) %% d = p %% d + q %% d.
 Proof.
 have [-> | dn0] := eqVneq d 0; first by rewrite !modp0.
-by apply: IdomainUnit.modp_add; rewrite unitfE lead_coef_eq0.
+by apply: IdomainUnit.modpD; rewrite unitfE lead_coef_eq0.
 Qed.
 
-Lemma modp_opp p q : (- p) %% q = - (p %% q).
-Proof. by apply/eqP; rewrite -addr_eq0 -modp_add addNr mod0p. Qed.
+Lemma modpN p q : (- p) %% q = - (p %% q).
+Proof. by apply/eqP; rewrite -addr_eq0 -modpD addNr mod0p. Qed.
 
-Lemma modNp p q : (- p) %% q = - (p %% q). Proof. exact: modp_opp. Qed.
+Lemma modNp p q : (- p) %% q = - (p %% q). Proof. exact: modpN. Qed.
 
-Lemma divp_add d p q : (p + q) %/ d = p %/ d + q %/ d.
+Lemma divpD d p q : (p + q) %/ d = p %/ d + q %/ d.
 Proof.
 have [-> | dn0] := eqVneq d 0; first by rewrite !divp0 addr0.
-by apply: IdomainUnit.divp_add; rewrite unitfE lead_coef_eq0.
+by apply: IdomainUnit.divpD; rewrite unitfE lead_coef_eq0.
 Qed.
 
-Lemma divp_opp p q : (- p) %/ q = - (p %/ q).
-Proof. by apply/eqP; rewrite -addr_eq0 -divp_add addNr div0p. Qed.
+Lemma divpN p q : (- p) %/ q = - (p %/ q).
+Proof. by apply/eqP; rewrite -addr_eq0 -divpD addNr div0p. Qed.
 
 Lemma divp_addl_mul_small d q r : size r < size d -> (q * d + r) %/ d = q.
 Proof.
-move=> srd; rewrite divp_add (divp_small srd) addr0 mulpK //.
-by rewrite -size_poly_gt0; apply: leq_trans srd.
+move=> srd; rewrite divpD (divp_small srd) addr0 mulpK // -size_poly_gt0.
+exact: leq_trans srd.
 Qed.
 
 Lemma modp_addl_mul_small d q r : size r < size d -> (q * d + r) %% d = r.
-Proof. by move=> srd; rewrite modp_add modp_mull add0r modp_small. Qed.
+Proof. by move=> srd; rewrite modpD modp_mull add0r modp_small. Qed.
 
 Lemma divp_addl_mul d q r : d != 0 -> (q * d + r) %/ d = q + r %/ d.
-Proof. by move=> dn0; rewrite divp_add mulpK. Qed.
+Proof. by move=> dn0; rewrite divpD mulpK. Qed.
 
 Lemma divpp d : d != 0 -> d %/ d = 1.
 Proof.
@@ -2962,9 +3026,7 @@ by rewrite -size_poly_gt0; apply: leq_trans srd.
 Qed.
 
 Lemma modp_mul p q m : (p * (q %% m)) %% m = (p * q) %% m.
-Proof.
-by rewrite [in RHS](divp_eq q m) mulrDr modp_add mulrA modp_mull add0r.
-Qed.
+Proof. by rewrite [in RHS](divp_eq q m) mulrDr modpD mulrA modp_mull add0r. Qed.
 
 Lemma dvdpP p q : reflect (exists qq, p = qq * q) (q %| p).
 Proof.
@@ -3131,6 +3193,31 @@ End FieldMap.
 
 End FieldDivision.
 
+Notation "@ 'modp_scalel'" :=
+  (deprecate modp_scalel modpZl) (at level 10, only parsing) : fun_scope.
+Notation "@ 'modp_scaler'" :=
+  (deprecate modp_scaler modpZr) (at level 10, only parsing) : fun_scope.
+Notation "@ 'modp_opp'" :=
+  (deprecate modp_opp modpN) (at level 10, only parsing) : fun_scope.
+Notation "@ 'modp_add'" :=
+  (deprecate modp_add modpD) (at level 10, only parsing) : fun_scope.
+Notation "@ 'divp_scalel'" :=
+  (deprecate modp_scalel divpZl) (at level 10, only parsing) : fun_scope.
+Notation "@ 'divp_scaler'" :=
+  (deprecate modp_scaler divpZr) (at level 10, only parsing) : fun_scope.
+Notation "@ 'divp_opp'" :=
+  (deprecate modp_opp divpN) (at level 10, only parsing) : fun_scope.
+Notation "@ 'divp_add'" :=
+  (deprecate modp_add divpD) (at level 10, only parsing) : fun_scope.
+Notation modp_scalel := (@modp_scalel _) (only parsing).
+Notation modp_scaler := (@modp_scaler _ _) (only parsing).
+Notation modp_opp := (@modp_opp _) (only parsing).
+Notation modp_add := (@modp_add _) (only parsing).
+Notation divp_scalel := (@divp_scalel _) (only parsing).
+Notation divp_scaler := (@divp_scaler _ _) (only parsing).
+Notation divp_opp := (@divp_opp _) (only parsing).
+Notation divp_add := (@divp_add _) (only parsing).
+
 End Field.
 
 Module ClosedField.
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 5680a24..b449d66 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -4693,7 +4693,7 @@ Lemma natf_neq0 n : (n%:R != 0 :> R) = [char R]^'.-nat n.
 Proof.
 have [-> | /prod_prime_decomp->] := posnP n; first by rewrite eqxx.
 rewrite !big_seq; elim/big_rec: _ => [|[p e] s /=]; first by rewrite oner_eq0.
-case/mem_prime_decomp=> p_pr _ _; rewrite pnat_mul pnat_exp eqn0Ngt orbC => <-.
+case/mem_prime_decomp=> p_pr _ _; rewrite pnatM pnatX eqn0Ngt orbC => <-.
 by rewrite natrM natrX mulf_eq0 expf_eq0 negb_or negb_and pnatE ?inE p_pr.
 Qed.
 
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index f54a957..6d7899b 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -1005,24 +1005,17 @@ Lemma expr1z x : x ^ 1 = x. Proof. by []. Qed.
 Lemma exprN1 x : x ^ (-1) = x^-1. Proof. by []. Qed.
 
 Lemma invr_expz x n : (x ^ n)^-1 = x ^ (- n).
-Proof.
-by case: (intP n)=> // [|m]; rewrite ?opprK ?expr0z ?invr1 // invrK.
-Qed.
+Proof. by case: (intP n)=> // [|m]; rewrite ?opprK ?expr0z ?invr1 // invrK. Qed.
 
 Lemma exprz_inv x n : (x^-1) ^ n = x ^ (- n).
-Proof.
-by case: (intP n)=> // m; rewrite -[_ ^ (- _)]exprVn ?opprK ?invrK.
-Qed.
+Proof. by case: (intP n)=> // m; rewrite -[_ ^ (- _)]exprVn ?opprK ?invrK. Qed.
 
 Lemma exp1rz n : 1 ^ n = 1 :> R.
-Proof.
-by case: (intP n)=> // m; rewrite -?exprz_inv ?invr1; apply: expr1n.
-Qed.
+Proof. by case: (intP n)=> // m; rewrite -?exprz_inv ?invr1; apply: expr1n. Qed.
 
 Lemma exprSz x (n : nat) : x ^ n.+1 = x * x ^ n. Proof. exact: exprS. Qed.
 
-Lemma exprSzr x (n : nat) : x ^ n.+1 = x ^ n * x.
-Proof. exact: exprSr. Qed.
+Lemma exprSzr x (n : nat) : x ^ n.+1 = x ^ n * x. Proof. exact: exprSr. Qed.
 
 Fact exprzD_nat x (m n : nat) : x ^ (m%:Z + n) = x ^ m * x ^ n.
 Proof. exact: exprD. Qed.
@@ -1682,7 +1675,7 @@ Proof.
 wlog le_n21: n1 n2 / n2 <= n1.
   move=> IH; case/orP: (leq_total n2 n1) => /IH //.
   by rewrite (addnC (n2 ^ 2)) (mulnC n2) distnC.
-by rewrite distnEl ?sqrn_sub ?subnK ?nat_Cauchy.
+by rewrite distnEl ?sqrnB ?subnK ?nat_Cauchy.
 Qed.
 
 End Distn.
@@ -1718,11 +1711,8 @@ Implicit Types p q r : {poly R}.
 Lemma coefMrz : forall p n i, (p *~ n)`_i = (p`_i *~ n).
 Proof. by move=> p [] n i; rewrite ?NegzE (coefMNn, coefMn). Qed.
 
-Lemma polyC_mulrz : forall n, {morph (@polyC R) : c / c *~ n}.
-Proof.
-move=> [] n c; rewrite ?NegzE -?pmulrn ?polyC_muln //.
-by rewrite polyC_opp mulrNz polyC_muln nmulrn.
-Qed.
+Lemma polyCMz : forall n, {morph (@polyC R) : c / c *~ n}.
+Proof. by case/intP => // n c; rewrite ?mulrNz -!pmulrn ?polyCN ?polyCMn. Qed.
 
 Lemma hornerMz : forall n (p : {poly R}) x, (p *~ n).[x] = p.[x] *~ n.
 Proof. by case=> *; rewrite ?NegzE ?mulNzr ?(hornerN, hornerMn). Qed.
@@ -1740,7 +1730,7 @@ Section PolyZintOIdom.
 Variable R : realDomainType.
 
 Lemma mulpz (p : {poly R}) (n : int) : p *~ n = n%:~R *: p.
-Proof. by rewrite -[p *~ n]mulrzl -mul_polyC polyC_mulrz polyC1. Qed.
+Proof. by rewrite -[p *~ n]mulrzl -mul_polyC polyCMz polyC1. Qed.
 
 End PolyZintOIdom.
 
@@ -1787,3 +1777,7 @@ Lemma rpredXsign R S (divS : @divrPred R S) (kS : keyed_pred divS) n x :
 Proof. by rewrite -signr_odd; case: (odd n); rewrite ?rpredV. Qed.
 
 End rpred.
+
+Notation "@ 'polyC_mulrz'" :=
+  (deprecate polyC_mulrz polyCMz) (at level 10, only parsing) : fun_scope.
+Notation polyC_mulrz := (@polyC_mulrz _) (only parsing).
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index 21394bd..462f8ad 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -1491,7 +1491,7 @@ move=> eq_fg; apply/vspaceP=> y.
 by apply/memv_imgP/memv_imgP=> [][x Vx ->]; exists x; rewrite ?eq_fg.
 Qed.
 
-Lemma limg_add f : {morph lfun_img f : U V / U + V}%VS.
+Lemma limgD f : {morph lfun_img f : U V / U + V}%VS.
 Proof.
 move=> U V; apply/eqP; rewrite unlock eqEsubv /subsetv /= -genmx_adds.
 by rewrite !genmxE !(eqmxMr _ (genmxE _)) !addsmxMr submx_refl.
@@ -1499,7 +1499,7 @@ Qed.
 
 Lemma limg_sum f I r (P : pred I) Us :
   (f @: (\sum_(i <- r | P i) Us i) = \sum_(i <- r | P i) f @: Us i)%VS.
-Proof. exact: (big_morph _ (limg_add f) (limg0 f)). Qed.
+Proof. exact: (big_morph _ (limgD f) (limg0 f)). Qed.
 
 Lemma limg_cap f U V : (f @: (U :&: V) <= f @: U :&: f @: V)%VS.
 Proof. by rewrite subv_cap !limgS ?capvSl ?capvSr. Qed.
@@ -1551,7 +1551,7 @@ Proof. by apply: (iffP subvP) => E x /E/eqlfunP. Qed.
 
 Lemma limg_ker_compl f U : (f @: (U :\: lker f) = f @: U)%VS.
 Proof.
-rewrite -{2}(addv_diff_cap U (lker f)) limg_add; apply/esym/addv_idPl.
+rewrite -{2}(addv_diff_cap U (lker f)) limgD; apply/esym/addv_idPl.
 by rewrite (subv_trans _ (sub0v _)) // subv0 -lkerE capvSr.
 Qed.
 
@@ -1701,7 +1701,7 @@ Proof. by move=> sVW; rewrite addvS // limgS // capvS. Qed.
 
 Lemma lpreimK f W : (W <= limg f)%VS -> (f @: (f @^-1: W))%VS = W.
 Proof.
-move=> sWf; rewrite limg_add (capv_idPl sWf) // -limg_comp.
+move=> sWf; rewrite limgD (capv_idPl sWf) // -limg_comp.
 have /eqP->: (f @: lker f == 0)%VS by rewrite -lkerE.
 have /andP[/eqP defW _] := vbasisP W; rewrite addv0 -defW limg_span.
 rewrite map_id_in // => x Xx; rewrite lfunE /= limg_lfunVK //.
@@ -2044,3 +2044,7 @@ by apply/ffunP=> i; rewrite (lfunE (Linear lhsZ)) !ffunE sol_u.
 Qed.
 
 End Solver.
+
+Notation "@ 'limg_add'" :=
+  (deprecate limg_add limgD) (at level 10, only parsing) : fun_scope.
+Notation limg_add := (@limg_add _ _ _) (only parsing).
diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v
index 015d971..505fda9 100644
--- a/mathcomp/algebra/zmodp.v
+++ b/mathcomp/algebra/zmodp.v
@@ -142,7 +142,7 @@ Proof. by move=> Ux; rewrite /= Zp_mulC Zp_mulVz. Qed.
 Lemma Zp_intro_unit x y : Zp_mul y x = Zp1 -> coprime p x.
 Proof.
 case=> yx1; have:= coprimen1 p.
-by rewrite -coprime_modr -yx1 coprime_modr coprime_mulr; case/andP.
+by rewrite -coprime_modr -yx1 coprime_modr coprimeMr; case/andP.
 Qed.
 
 Lemma Zp_inv_out x : ~~ coprime p x -> Zp_inv x = x.