fixes #1241

CHANGELOG_UNRELEASED.md

@@ -8,6 +8,25 @@
 
 ### Renamed
 
+- in `constructive_ereal.v`:
+  + `lte_pdivr_mull` -> `lte_pdivrMl`
+  + `lte_pdivr_mulr` -> `lte_pdivrMr`
+  + `lte_pdivl_mull` -> `lte_pdivlMl`
+  + `lte_pdivl_mulr` -> `lte_pdivlMr`
+  + `lte_ndivl_mulr` -> `lte_ndivlMr`
+  + `lte_ndivl_mull` -> `lte_ndivlMl`
+  + `lte_ndivr_mull` -> `lte_ndivrMl`
+  + `lte_ndivr_mulr` -> `lte_ndivrMr`
+  + `lee_pdivr_mull` -> `lee_pdivrMl`
+  + `lee_pdivr_mulr` -> `lee_pdivrMr`
+  + `lee_pdivl_mull` -> `lee_pdivlMl`
+  + `lee_pdivl_mulr` -> `lee_pdivlMr`
+  + `lee_ndivl_mulr` -> `lee_ndivlMr`
+  + `lee_ndivl_mull` -> `lee_ndivlMl`
+  + `lee_ndivr_mull` -> `lee_ndivrMl`
+  + `lee_ndivr_mulr` -> `lee_ndivrMr`
+  + `eqe_pdivr_mull` -> `eqe_pdivrMl`
+
 ### Generalized
 
 ### Deprecated

theories/constructive_ereal.v

@@ -3143,7 +3143,7 @@ move: x y => [x||] [y||] // in x0 h *.
 - by have := h _ h01; rewrite mulr_infty sgrV gtr0_sg // mul1e.
 Qed.
 
-Lemma lte_pdivr_mull r x y : (0 < r)%R -> (r^-1%:E * y < x) = (y < r%:E * x).
+Lemma lte_pdivrMl r x y : (0 < r)%R -> (r^-1%:E * y < x) = (y < r%:E * x).
 Proof.
 move=> r0; move: x y => [x| |] [y| |] //=.
 - by rewrite 2!lte_fin ltr_pdivrMl.
@@ -3157,10 +3157,10 @@ move=> r0; move: x y => [x| |] [y| |] //=.
 - by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e.
 Qed.
 
-Lemma lte_pdivr_mulr r x y : (0 < r)%R -> (y * r^-1%:E < x) = (y < x * r%:E).
-Proof. by move=> r0; rewrite muleC lte_pdivr_mull// muleC. Qed.
+Lemma lte_pdivrMr r x y : (0 < r)%R -> (y * r^-1%:E < x) = (y < x * r%:E).
+Proof. by move=> r0; rewrite muleC lte_pdivrMl// muleC. Qed.
 
-Lemma lte_pdivl_mull r y x : (0 < r)%R -> (x < r^-1%:E * y) = (r%:E * x < y).
+Lemma lte_pdivlMl r y x : (0 < r)%R -> (x < r^-1%:E * y) = (r%:E * x < y).
 Proof.
 move=> r0; move: x y => [x| |] [y| |] //=.
 - by rewrite 2!lte_fin ltr_pdivlMl.
@@ -3174,78 +3174,112 @@ move=> r0; move: x y => [x| |] [y| |] //=.
 - by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e.
 Qed.
 
-Lemma lte_pdivl_mulr r x y : (0 < r)%R -> (x < y * r^-1%:E) = (x * r%:E < y).
-Proof. by move=> r0; rewrite muleC lte_pdivl_mull// muleC. Qed.
+Lemma lte_pdivlMr r x y : (0 < r)%R -> (x < y * r^-1%:E) = (x * r%:E < y).
+Proof. by move=> r0; rewrite muleC lte_pdivlMl// muleC. Qed.
 
-Lemma lte_ndivl_mulr r x y : (r < 0)%R -> (x < y * r^-1%:E) = (y < x * r%:E).
+Lemma lte_ndivlMr r x y : (r < 0)%R -> (x < y * r^-1%:E) = (y < x * r%:E).
 Proof.
 rewrite -oppr0 ltrNr => r0; rewrite -{1}(opprK r) invrN.
-by rewrite EFinN muleN lteNr lte_pdivr_mulr// EFinN muleNN.
+by rewrite EFinN muleN lteNr lte_pdivrMr// EFinN muleNN.
 Qed.
 
-Lemma lte_ndivl_mull r x y : (r < 0)%R -> (x < r^-1%:E * y) = (y < r%:E * x).
-Proof. by move=> r0; rewrite muleC lte_ndivl_mulr// muleC. Qed.
+Lemma lte_ndivlMl r x y : (r < 0)%R -> (x < r^-1%:E * y) = (y < r%:E * x).
+Proof. by move=> r0; rewrite muleC lte_ndivlMr// muleC. Qed.
 
-Lemma lte_ndivr_mull r x y : (r < 0)%R -> (r^-1%:E * y < x) = (r%:E * x < y).
+Lemma lte_ndivrMl r x y : (r < 0)%R -> (r^-1%:E * y < x) = (r%:E * x < y).
 Proof.
 rewrite -oppr0 ltrNr => r0; rewrite -{1}(opprK r) invrN.
-by rewrite EFinN mulNe lteNl lte_pdivl_mull// EFinN muleNN.
+by rewrite EFinN mulNe lteNl lte_pdivlMl// EFinN muleNN.
 Qed.
 
-Lemma lte_ndivr_mulr r x y : (r < 0)%R -> (y * r^-1%:E < x) = (x * r%:E < y).
-Proof. by move=> r0; rewrite muleC lte_ndivr_mull// muleC. Qed.
+Lemma lte_ndivrMr r x y : (r < 0)%R -> (y * r^-1%:E < x) = (x * r%:E < y).
+Proof. by move=> r0; rewrite muleC lte_ndivrMl// muleC. Qed.
 
-Lemma lee_pdivr_mull r x y : (0 < r)%R -> (r^-1%:E * y <= x) = (y <= r%:E * x).
+Lemma lee_pdivrMl r x y : (0 < r)%R -> (r^-1%:E * y <= x) = (y <= r%:E * x).
 Proof.
 move=> r0; apply/idP/idP.
-- rewrite le_eqVlt => /predU1P[<-|]; last by rewrite lte_pdivr_mull// => /ltW.
+- rewrite le_eqVlt => /predU1P[<-|]; last by rewrite lte_pdivrMl// => /ltW.
   by rewrite muleA -EFinM divrr ?mul1e// unitfE gt_eqF.
-- rewrite le_eqVlt => /predU1P[->|]; last by rewrite -lte_pdivr_mull// => /ltW.
+- rewrite le_eqVlt => /predU1P[->|]; last by rewrite -lte_pdivrMl// => /ltW.
   by rewrite muleA -EFinM mulVr ?mul1e// unitfE gt_eqF.
 Qed.
 
-Lemma lee_pdivr_mulr r x y : (0 < r)%R -> (y * r^-1%:E <= x) = (y <= x * r%:E).
-Proof. by move=> r0; rewrite muleC lee_pdivr_mull// muleC. Qed.
+Lemma lee_pdivrMr r x y : (0 < r)%R -> (y * r^-1%:E <= x) = (y <= x * r%:E).
+Proof. by move=> r0; rewrite muleC lee_pdivrMl// muleC. Qed.
 
-Lemma lee_pdivl_mull r y x : (0 < r)%R -> (x <= r^-1%:E * y) = (r%:E * x <= y).
+Lemma lee_pdivlMl r y x : (0 < r)%R -> (x <= r^-1%:E * y) = (r%:E * x <= y).
 Proof.
 move=> r0; apply/idP/idP.
-- rewrite le_eqVlt => /predU1P[->|]; last by rewrite lte_pdivl_mull// => /ltW.
+- rewrite le_eqVlt => /predU1P[->|]; last by rewrite lte_pdivlMl// => /ltW.
   by rewrite muleA -EFinM divrr ?mul1e// unitfE gt_eqF.
-- rewrite le_eqVlt => /predU1P[<-|]; last by rewrite -lte_pdivl_mull// => /ltW.
+- rewrite le_eqVlt => /predU1P[<-|]; last by rewrite -lte_pdivlMl// => /ltW.
   by rewrite muleA -EFinM mulVr ?mul1e// unitfE gt_eqF.
 Qed.
 
-Lemma lee_pdivl_mulr r x y : (0 < r)%R -> (x <= y * r^-1%:E) = (x * r%:E <= y).
-Proof. by move=> r0; rewrite muleC lee_pdivl_mull// muleC. Qed.
+Lemma lee_pdivlMr r x y : (0 < r)%R -> (x <= y * r^-1%:E) = (x * r%:E <= y).
+Proof. by move=> r0; rewrite muleC lee_pdivlMl// muleC. Qed.
 
-Lemma lee_ndivl_mulr r x y : (r < 0)%R -> (x <= y * r^-1%:E) = (y <= x * r%:E).
+Lemma lee_ndivlMr r x y : (r < 0)%R -> (x <= y * r^-1%:E) = (y <= x * r%:E).
 Proof.
 rewrite -oppr0 ltrNr => r0; rewrite -{1}(opprK r) invrN.
-by rewrite EFinN muleN leeNr lee_pdivr_mulr// EFinN muleNN.
+by rewrite EFinN muleN leeNr lee_pdivrMr// EFinN muleNN.
 Qed.
 
-Lemma lee_ndivl_mull r x y : (r < 0)%R -> (x <= r^-1%:E * y) = (y <= r%:E * x).
-Proof. by move=> r0; rewrite muleC lee_ndivl_mulr// muleC. Qed.
+Lemma lee_ndivlMl r x y : (r < 0)%R -> (x <= r^-1%:E * y) = (y <= r%:E * x).
+Proof. by move=> r0; rewrite muleC lee_ndivlMr// muleC. Qed.
 
-Lemma lee_ndivr_mull r x y : (r < 0)%R -> (r^-1%:E * y <= x) = (r%:E * x <= y).
+Lemma lee_ndivrMl r x y : (r < 0)%R -> (r^-1%:E * y <= x) = (r%:E * x <= y).
 Proof.
 rewrite -oppr0 ltrNr => r0; rewrite -{1}(opprK r) invrN.
-by rewrite EFinN mulNe leeNl lee_pdivl_mull// EFinN muleNN.
+by rewrite EFinN mulNe leeNl lee_pdivlMl// EFinN muleNN.
 Qed.
 
-Lemma lee_ndivr_mulr r x y : (r < 0)%R -> (y * r^-1%:E <= x) = (x * r%:E <= y).
-Proof. by move=> r0; rewrite muleC lee_ndivr_mull// muleC. Qed.
+Lemma lee_ndivrMr r x y : (r < 0)%R -> (y * r^-1%:E <= x) = (x * r%:E <= y).
+Proof. by move=> r0; rewrite muleC lee_ndivrMl// muleC. Qed.
 
-Lemma eqe_pdivr_mull r x y : (r != 0)%R ->
+Lemma eqe_pdivrMl r x y : (r != 0)%R ->
   ((r^-1)%:E * y == x) = (y == r%:E * x).
 Proof.
 rewrite neq_lt => /orP[|] r0.
-- by rewrite eq_le lee_ndivr_mull// lee_ndivl_mull// -eq_le.
-- by rewrite eq_le lee_pdivr_mull// lee_pdivl_mull// -eq_le.
+- by rewrite eq_le lee_ndivrMl// lee_ndivlMl// -eq_le.
+- by rewrite eq_le lee_pdivrMl// lee_pdivlMl// -eq_le.
 Qed.
 
 End realFieldType_lemmas.
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_pdivrMl`")]
+Notation lte_pdivr_mull := lte_pdivrMl (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_pdivrMr`")]
+Notation lte_pdivr_mulr := lte_pdivrMr (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_pdivlMl`")]
+Notation lte_pdivl_mull := lte_pdivlMl (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_pdivlMr`")]
+Notation lte_pdivl_mulr := lte_pdivlMr (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_pdivrMl`")]
+Notation lee_pdivr_mull := lee_pdivrMl (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_pdivrMr`")]
+Notation lee_pdivr_mulr := lee_pdivrMr (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_pdivlMl`")]
+Notation lee_pdivl_mull := lee_pdivlMl (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_pdivlMr`")]
+Notation lee_pdivl_mulr := lee_pdivlMr (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_ndivrMl`")]
+Notation lte_ndivr_mull := lte_ndivrMl (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_ndivrMr`")]
+Notation lte_ndivr_mulr := lte_ndivrMr (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_ndivlMl`")]
+Notation lte_ndivl_mull := lte_ndivlMl (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_ndivlMr`")]
+Notation lte_ndivl_mulr := lte_ndivlMr (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_ndivrMl`")]
+Notation lee_ndivr_mull := lee_ndivrMl (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_ndivrMr`")]
+Notation lee_ndivr_mulr := lee_ndivrMr (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_ndivlMl`")]
+Notation lee_ndivl_mull := lee_ndivlMl (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_ndivlMr`")]
+Notation lee_ndivl_mulr := lee_ndivlMr (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `eqe_pdivrMl`")]
+Notation eqe_pdivr_mull := eqe_pdivrMl (only parsing).
 
 Module DualAddTheoryRealField.
 

theories/hoelder.v

@@ -179,7 +179,7 @@ under eq_integral do rewrite EFinM muleC.
 have foo : \int[mu]_x (`|f x| `^ p)%:E < +oo.
   move/integrableP: ifp => -[_].
   by under eq_integral do rewrite gee0_abs// ?lee_fin ?powR_ge0//.
-rewrite integralZl//; apply/eqP; rewrite eqe_pdivr_mull ?mule1.
+rewrite integralZl//; apply/eqP; rewrite eqe_pdivrMl ?mule1.
 - by rewrite fineK// gt0_fin_numE.
 - by rewrite gt_eqF// fine_gt0// foo andbT.
 Qed.
@@ -423,14 +423,14 @@ suff : 'N_p%:E[(f \+ g)%R] `^ p <= ('N_p%:E[f] + 'N_p%:E[g]) *
     'N_p%:E[(f \+ g)%R] `^ p * (fine 'N_p%:E[(f \+ g)%R])^-1%:E.
   have [-> _|Nfg0] := eqVneq 'N_p%:E[(f \+ g)%R] 0.
     by rewrite adde_ge0 ?Lnorm_ge0.
-  rewrite lee_pdivl_mulr ?fine_gt0// ?lt0e ?Nfg0 ?Lnorm_ge0//.
+  rewrite lee_pdivlMr ?fine_gt0// ?lt0e ?Nfg0 ?Lnorm_ge0//.
   rewrite -{1}(@fineK _ ('N_p%:E[(f \+ g)%R] `^ p)); last first.
     by rewrite fin_num_poweR// ge0_fin_numE// Lnorm_ge0.
-  rewrite -(invrK (fine _)) lee_pdivr_mull; last first.
+  rewrite -(invrK (fine _)) lee_pdivrMl; last first.
     rewrite invr_gt0 fine_gt0// (poweR_lty _ Nfgoo) andbT poweR_gt0//.
     by rewrite lt0e Nfg0 Lnorm_ge0.
   rewrite fineK ?ge0_fin_numE ?Lnorm_ge0// => /le_trans; apply.
-  rewrite lee_pdivr_mull; last first.
+  rewrite lee_pdivrMl; last first.
     by rewrite fine_gt0// poweR_lty// andbT poweR_gt0// lt0e Nfg0 Lnorm_ge0.
   by rewrite fineK// 1?muleC// fin_num_poweR// ge0_fin_numE ?Lnorm_ge0.
 have p0 : (0 < p)%R by exact: (lt_trans _ p1).

theories/lebesgue_integral.v

@@ -2374,7 +2374,7 @@ near=> n; have [ifoo|] := ltP (\int[mu]_(x in D) f x) +oo; last first.
   by near: n; exists 1%N => // n /= n0; rewrite gtr0_sg// ?lte_fin// ltr0n.
 rewrite -(@fineK _ (\int[mu]_(x in D) f x)); last first.
   by rewrite fin_numElt ifoo (le_lt_trans _ if_gt0).
-rewrite -lee_pdivr_mulr//; last first.
+rewrite -lee_pdivrMr//; last first.
   by move: if_gt0 ifoo; case: (\int[mu]_(x in D) f x).
 near: n.
 exists `|reals.ceil (M * (fine (\int[mu]_(x in D) f x))^-1)|%N => //.
@@ -2619,7 +2619,7 @@ rewrite monotone_convergence //.
     by rewrite mulry gtr0_sg ?mul1e ?leey// ltr0n.
   exists `|reals.ceil (M / fine (mu D))|%N => // m /=.
   rewrite -(ler_nat R) => MDm; rewrite -(@fineK _ (mu D)) ?ge0_fin_numE//.
-  rewrite -lee_pdivr_mulr; last by rewrite fine_gt0// lt0e muD0 measure_ge0.
+  rewrite -lee_pdivrMr; last by rewrite fine_gt0// lt0e muD0 measure_ge0.
   rewrite lee_fin (le_trans _ MDm)//.
   by rewrite natr_absz (le_trans (ceil_ge _))// ler_int ler_norm.
 - by move=> n; exact: measurable_cst.
@@ -5175,7 +5175,7 @@ apply: (le_lt_trans (integral_le_bound (M *+ 2)%:E _ _ _ _)) => //.
 - by rewrite lee_fin mulrn_wge0// ltW.
 - apply: aeW => z [Ez _]; rewrite /= lee_fin mulr2n.
   by rewrite (le_trans (ler_normB _ _))// lerD.
-by rewrite -lte_pdivl_mull ?mulrn_wgt0// muleC -EFinM.
+by rewrite -lte_pdivlMl ?mulrn_wgt0// muleC -EFinM.
 Qed.
 
 End continuous_density_L1.
@@ -6029,7 +6029,7 @@ have ka_pos : fine k / a \is Num.pos.
 have k_fin_num : k \is a fin_num.
   by rewrite ge0_fin_numE ?locally_integrable_ltbally// integral_ge0.
 have kar : (0 < 2^-1 * (fine k / a) - r)%R.
-  move: afxr; rewrite -{1}(fineK k_fin_num) -lte_pdivr_mulr; last first.
+  move: afxr; rewrite -{1}(fineK k_fin_num) -lte_pdivrMr; last first.
     by rewrite fine_gt0// k_gt0/= ltey_eq k_fin_num.
   rewrite (lebesgue_measure_ball _ (ltW r0))//.
   rewrite -!EFinM !lte_fin -invf_div ltf_pV2 ?posrE ?pmulrn_lgt0//.
@@ -6038,7 +6038,7 @@ have kar : (0 < 2^-1 * (fine k / a) - r)%R.
 near (0%R : R)^'+ => d.
 have axrdk : a%:E < (fine (mu (ball x (r + d))))^-1%:E * k.
   rewrite lebesgue_measure_ball//; last by rewrite addr_ge0// ltW.
-  rewrite -(fineK k_fin_num) -lte_pdivr_mulr; last first.
+  rewrite -(fineK k_fin_num) -lte_pdivrMr; last first.
     by rewrite fine_gt0// k_gt0/= locally_integrable_ltbally.
   rewrite -!EFinM !lte_fin -invf_div ltf_pV2//; last first.
     by rewrite posrE fine_gt0// ltry andbT lte_fin pmulrn_lgt0// addr_gt0.
@@ -6086,7 +6086,7 @@ have r_proof x : HL f x > c%:E -> {r | (0 < r)%R &
   rewrite in_itv/= andbT => rg0 <-{y} Hc; exists r => //.
   rewrite -(@fineK _ (mu (ball x r))) ?ge0_fin_numE//; last first.
     by rewrite lebesgue_measure_ball ?ltry// ltW.
-  rewrite -lte_pdivl_mulr// 1?muleC// fine_gt0//.
+  rewrite -lte_pdivlMr// 1?muleC// fine_gt0//.
   by rewrite lebesgue_measure_ball 1?ltW// ltry lte_fin mulrn_wgt0.
 rewrite lebesgue_regularity_inner_sup//; last first.
   rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //.
@@ -6127,7 +6127,7 @@ rewrite !EFinM -muleA lee_wpmul2l//=.
 apply: (@le_trans _ _
     (\sum_(i <- E) c^-1%:E * \int[mu]_(y in B i) `|(f y)|%:E)).
   rewrite [in leLHS]big_seq [in leRHS]big_seq; apply: lee_sum => r /ED /Dsub /[!inE] rD.
-  by rewrite -lee_pdivr_mull ?invr_gt0// invrK /B/=; exact/ltW/cMfx_int.
+  by rewrite -lee_pdivrMl ?invr_gt0// invrK /B/=; exact/ltW/cMfx_int.
 rewrite -ge0_sume_distrr//; last by move=> x _; rewrite integral_ge0.
 rewrite lee_wpmul2l//; first by rewrite lee_fin invr_ge0 ltW.
 rewrite -ge0_integral_bigsetU//=.
@@ -6220,7 +6220,7 @@ near=> t.
 have [t0|t0] := leP t 0%R; first by rewrite /= davg0//= subrr normr0 ltW.
 rewrite sub0r normrN /= ger0_norm; last by rewrite fine_ge0// davg_ge0.
 rewrite -lee_fin fineK//; last by rewrite dfx//= sub0r normrN gtr0_norm.
-rewrite /davg/= /iavg/= lee_pdivr_mull//; last first.
+rewrite /davg/= /iavg/= lee_pdivrMl//; last first.
   by rewrite fine_gt0// lebesgue_measure_ball// ?ltry ?lte_fin ?mulrn_wgt0 ?ltW.
 rewrite (@le_trans _ _ (\int[mu]_(y in ball x t) e%:E))//.
   apply: ge0_le_integral => //=.
@@ -6577,7 +6577,7 @@ have HL_null n : mu (HLf_g_Be n) <= (3%:R / (e / 2))%:E * n.+1%:R^-1%:E.
   by rewrite indicE; case: (_ \in _) => /=; rewrite !(mulr1, mulr0).
 have fgn_null n : mu [set x | `|(f_ k \- g_B n) x|%:E >= (e / 2)%:E] <=
                      (e / 2)^-1%:E * n.+1%:R^-1%:E.
-  rewrite lee_pdivl_mull ?invr_gt0 ?divr_gt0// -[X in mu X]setTI.
+  rewrite lee_pdivlMl ?invr_gt0 ?divr_gt0// -[X in mu X]setTI.
   apply: le_trans.
     apply: (@le_integral_comp_abse _ _ _ mu _ measurableT
         (EFin \o (f_ k \- g_B n)%R) (e / 2) id) => //=.
@@ -6606,7 +6606,7 @@ rewrite (@le_trans _ _ ((4 / (e / 2))%:E * n.+1%:R^-1%:E))//.
   apply: le_trans; first by apply: leeD; [exact: HL_null|exact: fgn_null].
   rewrite -muleDl// lee_pmul2r// -EFinD lee_fin -{2}(mul1r (_^-1)) -div1r.
   by rewrite -mulrDl natr1.
-rewrite -lee_pdivl_mull ?divr_gt0// -EFinM lee_fin -(@invrK _ r).
+rewrite -lee_pdivlMl ?divr_gt0// -EFinM lee_fin -(@invrK _ r).
 rewrite -invrM ?unitfE ?gt_eqF ?invr_gt0 ?divr_gt0//.
 rewrite lef_pV2 ?posrE ?mulr_gt0 ?invr_gt0 ?divr_gt0//.
 by rewrite -(@natr1 _ n) -lerBlDr; near: n; exact: nbhs_infty_ger.
@@ -6773,7 +6773,7 @@ Lemma nicely_shrinking_gt0 x E : nicely_shrinking x E ->
   forall n, (0 < mu (E n))%E.
 Proof.
 move=> [mE [[C r_]]] [/= C_gt0 _ _ + ] n => /(_ n).
-rewrite lebesgue_measure_ball// -lee_pdivr_mull//.
+rewrite lebesgue_measure_ball// -lee_pdivrMl//.
 apply: lt_le_trans.
 by rewrite mule_gt0// lte_fin invr_gt0.
 Qed.

theories/lebesgue_measure.v

@@ -2392,7 +2392,7 @@ have {}ZNF5 : mu (Z r%:num) <=
   + apply: bigcup_measurable => k _; case: ifPn => // _.
     by apply: measurable_closure; exact: is_scale_ball.
 apply/(le_trans ZNF5).
-move/ltW: F5e; rewrite [in X in X -> _](@lee_pdivl_mull R 5%:R) ?ltr0n//.
+move/ltW: F5e; rewrite [in X in X -> _](@lee_pdivlMl R 5%:R) ?ltr0n//.
 rewrite -nneseriesZl//; last by move=> *; exact: esum_ge0.
 apply: le_trans; apply: lee_nneseries => //; first by move=> *; exact: esum_ge0.
 move=> n _.

theories/normedtype.v

@@ -2941,10 +2941,10 @@ move=> [s||]/=.
   by apply: near_fun => //=; apply: continuousM => //=; apply: cvg_cst.
 - rewrite gt0_muley ?lte_fin// => A [u [realu uA]].
   exists (r^-1 * u)%R; split; first by rewrite realM// realV realE ltW.
-  by move=> x rux; apply: uA; move: rux; rewrite EFinM lte_pdivr_mull.
+  by move=> x rux; apply: uA; move: rux; rewrite EFinM lte_pdivrMl.
 - rewrite gt0_muleNy ?lte_fin// => A [u [realu uA]].
   exists (r^-1 * u)%R; split; first by rewrite realM// realV realE ltW.
-  by move=> x xru; apply: uA; move: xru; rewrite EFinM lte_pdivl_mull.
+  by move=> x xru; apply: uA; move: xru; rewrite EFinM lte_pdivlMl.
 Unshelve. all: by end_near. Qed.
 
 Lemma cvgeMl f x y : y \is a fin_num ->
@@ -2981,7 +2981,7 @@ Proof.
 move=> b_gt0 /cvgeyPge foo /fine_cvgP[gfin gb]; apply/cvgeyPgey.
 near (0%R : R)^'+ => e; near=> A; near=> n.
 rewrite (@le_trans _ _ (f n * e%:E))// ?lee_pmul// ?lee_fin//.
-- by rewrite -lee_pdivr_mulr ?divr_gt0//; near: n; apply: foo.
+- by rewrite -lee_pdivrMr ?divr_gt0//; near: n; apply: foo.
 - by rewrite (@le_trans _ _ 1) ?lee_fin//; near: n; apply: foo.
 rewrite -(@fineK _ (g n)) ?lee_fin; last by near: n; exact: gfin.
 by near: n; apply: (cvgr_ge b).
@@ -2993,7 +2993,7 @@ Proof.
 move=> b0 /cvgeyPge foo /fine_cvgP -[gfin gb]; apply/cvgeNyPleNy.
 near (0%R : R)^'+ => e; near=> A; near=> n.
 rewrite -leeN2 -muleN (@le_trans _ _ (f n * e%:E))//.
-  by rewrite -lee_pdivr_mulr ?mulr_gt0 ?oppr_gt0//; near: n; apply: foo.
+  by rewrite -lee_pdivrMr ?mulr_gt0 ?oppr_gt0//; near: n; apply: foo.
 rewrite lee_pmul ?lee_fin//.
   by rewrite (@le_trans _ _ 1) ?lee_fin//; near: n; apply: foo.
 rewrite -(@fineK _ (g n)) ?lee_fin; last by near: n; exact: gfin.
@@ -3270,7 +3270,7 @@ have : (edist (x, y) <= (eps%:num / 2)%:E)%E.
   apply: ereal_inf_lb; exists (eps%:num / 2) => //; split => //.
   exact: (bxy (eps%:num / 2)%:pos).
 apply: contra_leP => _.
-by rewrite /= EFinM fineK// lte_pdivr_mulr// lte_pmulr// lte1n.
+by rewrite /= EFinM fineK// lte_pdivrMr// lte_pmulr// lte1n.
 Qed.
 
 Lemma edist_refl x : edist (x, x) = 0%E. Proof. exact/edist_closeP. Qed.