less unitfE (#1571)

pi8027 · affeldt-aist · web-flow · commit d8087fdbce2d · 2025-07-03T09:27:09.000+09:00
Co-authored-by: Reynald Affeldt &lt;reynald.affeldt@aist.go.jp&gt;
diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v
@@ -3533,21 +3533,21 @@ move=> x0; apply/(iffP idP) => [xy r /andP[r0 r1]|h].
   move: x0 xy; rewrite le_eqVlt => /predU1P[<-|x0 xy]; first by rewrite mule0.
   by rewrite (le_trans _ xy)// gee_pMl// ltW.
 have h01 : (0 < (2^-1 : R) < 1)%R by rewrite invr_gt0 ?invf_lt1 ?ltr0n ?ltr1n.
-move: x y => [x||] [y||] // in x0 h *.
-- move: (x0); rewrite lee_fin le_eqVlt => /predU1P[<-|{}x0].
-    by rewrite (le_trans _ (h _ h01))// mule_ge0// lee_fin.
-  have y0 : (0 < y)%R.
-    by rewrite -lte_fin (lt_le_trans _ (h _ h01))// mule_gt0// lte_fin.
-  rewrite lee_fin leNgt; apply/negP => yx.
-  have /h : (0 < (y + x) / (2 * x) < 1)%R.
-    rewrite ltr_pdivlMr ?ltr_pdivrMr ?mulr_gt0// mul0r mul1r.
-    by rewrite mulr_natl mulr2n ltrD2r yx addr_gt0.
-  rewrite -(EFinM _ x) lee_fin invrM ?unitfE// ?gt_eqF// -mulrA mulrAC.
-  by rewrite mulVr ?unitfE ?gt_eqF// mul1r; apply/negP; rewrite -ltNge midf_lt.
+move: x y => [x||] [y||] // in x0 h *; last 4 first.
 - by rewrite leey.
 - by have := h _ h01.
 - by have := h _ h01; rewrite mulr_infty sgrV gtr0_sg // mul1e.
 - by have := h _ h01; rewrite mulr_infty sgrV gtr0_sg // mul1e.
+move: (x0); rewrite lee_fin le_eqVlt => /predU1P[<-|{}x0].
+  by rewrite (le_trans _ (h _ h01))// mule_ge0// lee_fin.
+have y0 : (0 < y)%R.
+  by rewrite -lte_fin (lt_le_trans _ (h _ h01))// mule_gt0// lte_fin.
+rewrite lee_fin leNgt; apply/negP => yx.
+have /h : (0 < (y + x) / (2 * x) < 1)%R.
+  apply/andP; split; first by rewrite divr_gt0 // ?addr_gt0// ?mulr_gt0.
+  by rewrite ltr_pdivrMr ?mulr_gt0// mul1r mulr_natl mulr2n ltrD2r.
+rewrite -EFinM lee_fin invfM -mulrA divfK ?gt_eqF//.
+by apply/negP; rewrite -ltNge midf_lt.
 Qed.
 
 Lemma lte_pdivrMl r x y : (0 < r)%R -> (r^-1%:E * y < x) = (y < r%:E * x).
@@ -3606,9 +3606,9 @@ 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_pdivrMl// => /ltW.
-  by rewrite muleA -EFinM divrr ?mul1e// unitfE gt_eqF.
+  by rewrite muleA -EFinM divff ?mul1e// gt_eqF.
 - rewrite le_eqVlt => /predU1P[->|]; last by rewrite -lte_pdivrMl// => /ltW.
-  by rewrite muleA -EFinM mulVr ?mul1e// unitfE gt_eqF.
+  by rewrite muleA -EFinM mulVf ?mul1e// gt_eqF.
 Qed.
 
 Lemma lee_pdivrMr r x y : (0 < r)%R -> (y * r^-1%:E <= x) = (y <= x * r%:E).
@@ -3618,9 +3618,9 @@ 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_pdivlMl// => /ltW.
-  by rewrite muleA -EFinM divrr ?mul1e// unitfE gt_eqF.
+  by rewrite muleA -EFinM divff ?mul1e// gt_eqF.
 - rewrite le_eqVlt => /predU1P[<-|]; last by rewrite -lte_pdivlMl// => /ltW.
-  by rewrite muleA -EFinM mulVr ?mul1e// unitfE gt_eqF.
+  by rewrite muleA -EFinM mulVf ?mul1e// gt_eqF.
 Qed.
 
 Lemma lee_pdivlMr r x y : (0 < r)%R -> (x <= y * r^-1%:E) = (x * r%:E <= y).
@@ -4512,8 +4512,7 @@ Definition contract x : R :=
 
 Lemma contract_lt1 r : (`|contract r%:E| < 1)%R.
 Proof.
-rewrite normrM normrV ?unitfE //.
-rewrite ltr_pdivrMr // ?mul1r//; last by rewrite gtr0_norm.
+rewrite normrM normfV// ltr_pdivrMr // ?mul1r//; last by rewrite gtr0_norm.
 by rewrite [ltRHS]gtr0_norm ?ltrDr// ltr_pwDl.
 Qed.
 
@@ -4561,25 +4560,23 @@ move=> r; rewrite inE le_eqVlt => /orP[|r1].
     by [rewrite expand1|rewrite expandN1].
 rewrite /expand 2!leNgt ltrNl; case/ltr_normlP : (r1) => -> -> /=.
 have r_pneq0 : (1 + r / (1 - r) != 0)%R.
-  rewrite -[X in (X + _)%R](@divrr _ (1 - r)%R) -?mulrDl; last first.
-    by rewrite unitfE subr_eq0 eq_sym lt_eqF // ltr_normlW.
+  rewrite -[X in (X + _)%R](@divff _ (1 - r)%R) -?mulrDl; last first.
+    by rewrite subr_eq0 eq_sym lt_eqF // ltr_normlW.
   by rewrite subrK mulf_neq0 // invr_eq0 subr_eq0 eq_sym lt_eqF // ltr_normlW.
 have r_nneq0 : (1 - r / (1 + r) != 0)%R.
-  rewrite -[X in (X + _)%R](@divrr _ (1 + r)%R) -?mulrBl; last first.
-    by rewrite unitfE addrC addr_eq0 gt_eqF // ltrNnormlW.
-  rewrite addrK mulf_neq0 // invr_eq0 addr_eq0 -eqr_oppLR eq_sym gt_eqF //.
-  exact: ltrNnormlW.
+  rewrite -[X in (X + _)%R](@divff _ (1 + r)%R) -?mulrBl; last first.
+    by rewrite addrC addr_eq0 gt_eqF // ltrNnormlW.
+  by rewrite addrK mulf_neq0// invr_eq0 addr_eq0 -eqr_oppLR lt_eqF// ltrNnormlW.
 wlog : r r1 r_pneq0 r_nneq0 / (0 <= r)%R => wlog_r0.
   have [r0|r0] := lerP 0 r; first by rewrite wlog_r0.
   move: (wlog_r0 (- r)%R).
   rewrite !(normrN, opprK, mulNr) oppr_ge0 => /(_ r1 r_nneq0 r_pneq0 (ltW r0)).
-  by move/eqP; rewrite eqr_opp => /eqP.
+  by move/oppr_inj.
 rewrite /contract !ger0_norm //; last first.
   by rewrite divr_ge0 // subr_ge0 (le_trans _ (ltW r1)) // ler_norm.
-apply: (@mulIr _ (1 + r / (1 - r))%R); first by rewrite unitfE.
-rewrite -(mulrA (r / _)%R) mulVr ?unitfE // mulr1.
-rewrite -[X in (X + _ / _)%R](@divrr _ (1 - r)%R) -?mulrDl ?subrK ?div1r //.
-by rewrite unitfE subr_eq0 eq_sym lt_eqF // ltr_normlW.
+apply: (@mulIf _ (1 + r / (1 - r))%R); rewrite // divfK//.
+rewrite -[X in (X + _ / _)%R](@divff _ (1 - r)%R) -?mulrDl ?subrK ?div1r //.
+by rewrite subr_eq0 eq_sym lt_eqF // ltr_normlW.
 Qed.
 
 Lemma le_contract : {mono contract : x y / (x <= y)%O}.
diff --git a/theories/charge.v b/theories/charge.v
@@ -864,7 +864,7 @@ have : cvg (series (fun n => fine (maxe (z_ (v n) * 2^-1%:E) (- 1%E))) n @[n -->
 move/cvg_series_cvg_0 => maxe_cvg_0.
 apply: not_s_cvg_0.
 rewrite (_ : _ \o _ = (fun n => z_ (v n) * 2^-1%:E) \* cst 2%:E); last first.
-  by apply/funext => n/=; rewrite -muleA -EFinM mulVr ?mule1// unitfE.
+  by apply/funext => n/=; rewrite -muleA -EFinM mulVf ?mule1.
 rewrite (_ : 0 = 0 * 2%:E); last by rewrite mul0e.
 apply: cvgeM; [by rewrite mule_def_fin| |exact: cvg_cst].
 apply/fine_cvgP; split.
@@ -1586,8 +1586,8 @@ exists (PosNum e_gt0); rewrite ge0_integralD//; last 2 first.
 rewrite integral_cst// -lteBrDr//; last first.
   by rewrite fin_numM// fin_num_measure.
 rewrite -[X in _ * X](@fineK _ (mu A)) ?fin_num_measure//.
-rewrite -EFinM -mulrA mulVr ?mulr1; last first.
-  by rewrite unitfE gt_eqF// fine_gt0// muA_gt0/= ltey_eq fin_num_measure.
+rewrite -EFinM -mulrA mulVf ?mulr1; last first.
+  by rewrite gt_eqF// fine_gt0// muA_gt0/= ltey_eq fin_num_measure.
 rewrite lteBrDl// addeC -lteBrDl//; last first.
 rewrite -(@fineK _ (nu A))// ?fin_num_measure// -[X in _ - X](@fineK _)//.
 rewrite -EFinB lte_fin /mid ltr_pdivrMr// ltr_pMr// ?ltr1n// subr_gt0.
diff --git a/theories/derive.v b/theories/derive.v
@@ -341,8 +341,7 @@ rewrite add0r normrN normrZ -ltr_pdivlMl ?normr_gt0 ?invr_neq0 //.
 have /Hi/le_lt_trans -> // : ball 0 i (j *: v).
    by rewrite -ball_normE/= add0r normrN (le_lt_trans _ jvi) // normrZ.
 rewrite -(mulrC e) -mulrA -ltr_pdivlMl // mulrA mulVf ?gt_eqF//.
-rewrite normrV ?unitfE // div1r invrK ltr_pdivrMl; last first.
-  by rewrite pmulr_rgt0 // normr_gt0.
+rewrite normfV div1r invrK ltr_pdivrMl; last by rewrite pmulr_rgt0 // normr_gt0.
 rewrite normrZ mulrC -mulrA.
 by rewrite ltr_pMl ?ltr1n // pmulr_rgt0 ?normm_gt0 // normr_gt0.
 Qed.
@@ -709,8 +708,8 @@ suff /he : ball 0 e%:num (k^-1 *: x).
   rewrite -ball_normE /= distrC subr0 => /ltW /le_trans; apply.
   by rewrite ger0_norm /k // mulVf.
 rewrite -ball_normE /= distrC subr0 normrZ.
-rewrite normfV ger0_norm /k // invrM ?unitfE // mulrAC mulVf //.
-by rewrite invf_div mul1r [ltRHS]splitr; apply: ltr_pwDr.
+rewrite normfV ger0_norm /k // invfM/= -mulrA mulVf ?gt_eqF//.
+by rewrite mulr1 invf_div gtr_pMr// invf_lt1// ltr1n.
 Qed.
 
 Lemma linear_eqO (V' W' : normedModType R) (f : {linear V' -> W'}) :
@@ -784,10 +783,8 @@ suff /he : ball 0 e%:num (ku^-1 *: u, kv^-1 *: v).
   by rewrite mulrA [ku * _]mulrAC expr2.
 rewrite -ball_normE /= distrC subr0.
 have -> : (ku^-1 *: u, kv^-1 *: v) =
-  (e%:num / 2) *: ((PosNum un0)%:num ^-1 *: u, (PosNum vn0)%:num ^-1 *: v).
-  rewrite invrM ?unitfE // [kv ^-1]invrM ?unitfE //.
-  rewrite mulrC -[_ *: u]scalerA [X in X *: v]mulrC -[_ *: v]scalerA.
-  by rewrite invf_div.
+    (e%:num / 2) *: ((PosNum un0)%:num ^-1 *: u, (PosNum vn0)%:num ^-1 *: v).
+  by rewrite invfM [kv ^-1]invfM invf_div -[_ *: u]scalerA -[_ *: v]scalerA.
 rewrite normrZ ger0_norm // -mulrA gtr_pMr // ltr_pdivrMl // mulr1.
 by rewrite prod_normE/= !normrZ !normfV !normr_id !mulVf ?gt_eqF// maxxx ltr1n.
 Qed.
diff --git a/theories/exp.v b/theories/exp.v
@@ -1003,7 +1003,7 @@ rewrite le_eqVlt => /predU1P[<-|a0].
   by rewrite powR0 ?invr_eq0 ?pnatr_eq0// sqrtr0.
 have /eqP : (a `^ (2^-1)) ^+ 2 = (Num.sqrt a) ^+ 2.
   rewrite sqr_sqrtr; last exact: ltW.
-  by rewrite /powR gt_eqF// -expRM_natl mulrA divrr ?mul1r ?unitfE// lnK.
+  by rewrite /powR gt_eqF// -expRM_natl mulrA divff ?mul1r// lnK.
 rewrite eqf_sqr => /predU1P[//|/eqP h].
 have : 0 < a `^ 2^-1 by exact: powR_gt0.
 by rewrite h oppr_gt0 ltNge sqrtr_ge0.
diff --git a/theories/hoelder.v b/theories/hoelder.v
@@ -440,9 +440,9 @@ rewrite [leLHS](_ : _ = 'N_1[(F \* G)%R] * 'N_p%:E[f] * 'N_q%:E[g]); last first.
   rewrite -!muleA [X in _ * X](_ : _ = 1) ?mule1// EFinM muleACA.
   rewrite (_ : _ * 'N_p%:E[f] = 1) ?mul1e; last first.
     rewrite -[X in _ * X]fineK; last by rewrite ge0_fin_numE ?ltey// Lnorm_ge0.
-    by rewrite -EFinM mulVr ?unitfE ?gt_eqF// fine_gt0// fpos/= ltey.
+    by rewrite -EFinM mulVf ?gt_eqF// fine_gt0// fpos/= ltey.
   rewrite -[X in _ * X]fineK; last by rewrite ge0_fin_numE ?ltey// Lnorm_ge0.
-  by rewrite -EFinM mulVr ?unitfE ?gt_eqF// fine_gt0// gpos/= ltey.
+  by rewrite -EFinM mulVf ?gt_eqF// fine_gt0// gpos/= ltey.
 rewrite -(mul1e ('N_p%:E[f] * _)) -muleA lee_pmul ?mule_ge0 ?Lnorm_ge0//.
 rewrite [leRHS](_ : _ = \int[mu]_x (F x `^ p / p + G x `^ q / q)%:E).
   rewrite Lnorm1 ae_ge0_le_integral //.
diff --git a/theories/landau.v b/theories/landau.v
@@ -1334,8 +1334,8 @@ rewrite eqOmegaE eqOmegaO [in RHS]bigOE //.
 have [W1 k1 ?] := bigOmega; have [W2 k2 ?] := bigOmega.
 near=> k; near=> x; rewrite [`|_|]normrM.
 rewrite (@le_trans _ _ ((k2%:num * k1%:num)^-1 * `|(W1 * W2) x|)) //.
-  rewrite invrM ?unitfE ?gtr_eqF // -mulrA ler_pdivlMl //.
-  rewrite ler_pdivlMl // (mulrA k1%:num) mulrCA (@normrM _ (W1 x)).
+  rewrite invfM -mulrA ler_pdivlMl// ler_pdivlMl//.
+  rewrite (mulrCA k2%:num) (mulrA k1%:num) (@normrM _ (W1 x)).
   by rewrite ler_pM ?mulr_ge0 //; near: x.
 by rewrite ler_wpM2r // ltW //.
 Unshelve. all: by end_near. Qed.
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
@@ -626,14 +626,13 @@ rewrite itv_bnd_open_bigcup//; transitivity (limn (lebesgue_measure \o
   - by move=> ?; exact: measurable_itv.
   - by apply: bigcup_measurable => k _; exact: measurable_itv.
   - move=> n m nm; apply/subsetPset => x /=; rewrite !in_itv/= => /andP[->/=].
-    by move/le_trans; apply; rewrite lerB// ler_pV2 ?ler_nat//;
-      rewrite inE ltr0n andbT unitfE.
+    by move/le_trans; apply; rewrite lerB// lef_pV2 ?ler_nat ?posrE.
 rewrite (_ : _ \o _ = (fun n => (1 - n.+1%:R^-1)%:E)); last first.
   apply/funext => n /=; rewrite lebesgue_measure_itvoc.
   have [->|n0] := eqVneq n 0%N.
     by rewrite invr1 subrr set_itvoc0 wlength0.
   rewrite wlength_itv/= lte_fin ifT; last first.
-    by rewrite ler_ltB// invr_lt1 ?unitfE// ltr1n ltnS lt0n.
+    by rewrite ler_ltB// invf_lt1// ltr1n ltnS lt0n.
   by rewrite !(EFinB,EFinN) fin_num_oppeB// addeAC addeA subee// add0e.
 apply/cvg_lim => //=; apply/fine_cvgP; split => /=; first exact: nearW.
 apply/(@cvgrPdist_lt _ R^o) => _/posnumP[e].
diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v
@@ -995,7 +995,7 @@ move=> mf mg; rewrite (_ : (_ \* _) = (fun x => 2%:R^-1 * (f x + g x) ^+ 2)
     exact: measurableT_comp (exprn_measurable _) _.
 rewrite funeqE => x /=; rewrite -2!mulrBr sqrrD (addrC (f x ^+ 2)) -addrA.
 rewrite -(addrA (f x * g x *+ 2)) -opprB opprK (addrC (g x ^+ 2)) addrK.
-by rewrite -(mulr_natr (f x * g x)) -(mulrC 2) mulrA mulVr ?mul1r// unitfE.
+by rewrite -(mulr_natr (f x * g x)) -(mulrC 2) mulrA mulVf ?mul1r.
 Qed.
 
 Lemma measurable_fun_ltr D f g : measurable_fun D f -> measurable_fun D g ->
diff --git a/theories/measure.v b/theories/measure.v
@@ -3618,7 +3618,7 @@ Proof.
 rewrite /mnormalize; case: ifPn; first by rewrite probability_setT.
 rewrite negb_or => /andP[ft0 ftoo].
 have ? : mu setT \is a fin_num by rewrite ge0_fin_numE// ltey.
-by rewrite -{1}(@fineK _ (mu setT))// -EFinM divrr// ?unitfE fine_eq0.
+by rewrite -{1}(@fineK _ (mu setT))// -EFinM divff// fine_eq0.
 Qed.
 
 HB.instance Definition _ :=
diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
@@ -1975,7 +1975,7 @@ have [es|se] := leP s e%:num; last first.
   by apply: B0y; rewrite -ball_normE /ball_ /= distrC xye.
 exists (y + (s / 2) *: (`|x - y|^-1 *: (x - y))); split; [apply: Be|apply: B0y].
   rewrite /= opprD addrA -[X in `|X - _|](scale1r (x - y)) scalerA -scalerBl.
-  rewrite -[X in X - _](@divrr _ `|x - y|) ?unitfE ?normr_eq0 ?subr_eq0//.
+  rewrite -[X in X - _](@divff _ `|x - y|) ?normr_eq0 ?subr_eq0//.
   rewrite -mulrBl -scalerA normrZ normfZV ?subr_eq0// mulr1.
   rewrite gtr0_norm; first by rewrite ltrBlDl xye ltrDr mulr_gt0.
   by rewrite subr_gt0 xye ltr_pdivrMr // mulr_natr mulr2n ltr_pwDl.
diff --git a/theories/normedtype_theory/num_normedtype.v b/theories/normedtype_theory/num_normedtype.v
@@ -719,8 +719,8 @@ Notation near_in_itv := near_in_itvoo (only parsing).
 Lemma near_infty_natSinv_lt (R : archiFieldType) (e : {posnum R}) :
   \forall n \near \oo, n.+1%:R^-1 < e%:num.
 Proof.
-near=> n; rewrite -(@ltr_pM2r _ n.+1%:R) // mulVr ?unitfE //.
-rewrite -(@ltr_pM2l _ e%:num^-1) // mulr1 mulrA mulVr ?unitfE // mul1r.
+near=> n; rewrite -(@ltr_pM2r _ n.+1%:R) // mulVf.
+rewrite -(@ltr_pM2l _ e%:num^-1) // mulr1 mulrA mulVf// mul1r.
 rewrite (lt_trans (archi_boundP _)) // ltr_nat.
 by near: n; exists (Num.bound e%:num^-1).
 Unshelve. all: by end_near. Qed.
@@ -729,10 +729,10 @@ Lemma near_infty_natSinv_expn_lt (R : archiFieldType) (e : {posnum R}) :
   \forall n \near \oo, 1 / 2 ^+ n < e%:num.
 Proof.
 near=> n.
-rewrite -(@ltr_pM2r _ (2 ^+ n)) // -?natrX ?ltr0n ?expn_gt0//.
-rewrite mul1r mulVr ?unitfE ?gt_eqF// ?ltr0n ?expn_gt0//.
-rewrite -(@ltr_pM2l _ e%:num^-1) // mulr1 mulrA mulVr ?unitfE // mul1r.
-rewrite (lt_trans (archi_boundP _)) // natrX upper_nthrootP //.
+rewrite -(@ltr_pM2r _ (2 ^+ n))// -?natrX ?ltr0n ?expn_gt0//.
+rewrite mul1r mulVf ?gt_eqF//.
+rewrite -(@ltr_pM2l _ e%:num^-1)// mulr1 mulrA mulVf// mul1r.
+rewrite (lt_trans (archi_boundP _))// natrX upper_nthrootP//.
 near: n; eexists; last by move=> m; exact.
 by [].
 Unshelve. all: by end_near. Qed.
diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
@@ -412,8 +412,7 @@ apply/negPn/negP => /set0P[c] []; rewrite -ball_normE /ball_ => acr bcr.
 have r22 : r%:num * 2 = r%:num + r%:num.
   by rewrite (_ : 2 = 1 + 1) // mulrDr mulr1.
 move: (ltrD acr bcr); rewrite -r22 (distrC b c).
-move/(le_lt_trans (ler_distD c a b)).
-by rewrite -mulrA mulVr ?mulr1 ?ltxx // unitfE.
+by move/(le_lt_trans (ler_distD c a b)); rewrite -mulrA mulVf// mulr1 ltxx.
 Qed.
 Local Hint Extern 0 (hausdorff_space _) => solve[apply: norm_hausdorff] : core.
 
diff --git a/theories/normedtype_theory/vitali_lemma.v b/theories/normedtype_theory/vitali_lemma.v
@@ -535,7 +535,7 @@ have Bjrn : (radius (B j))%:num > r / (2 ^ n.+1)%:R.
 exists j; split => //.
 - by case: Dj => m /= mn Dm; exists m.
 - rewrite (le_trans _ (ltW Bjrn))// ler_pdivrMr// expnSr natrM.
-  by rewrite invrM ?unitfE// mulrAC -mulrA (mulrA 2) divff// div1r.
+  by rewrite invfM -!mulrA mulVf// mulr1.
 - move=> x Bix.
   rewrite is_ball_closure//; last first.
     by rewrite (ballE (is_ballB j)) scale_ballE; [exact: is_ball_ball|].
diff --git a/theories/numfun.v b/theories/numfun.v
@@ -575,7 +575,7 @@ move=> x Ax; have := fA1 _ Ax; rewrite 2!ler_norml => /andP[Mfx fxM].
 have [xL|xL] := leP (f x) (-(1/3) * M%:num).
   have: [set g x | x in A `&` f@^-1` `]-oo, -(1/3) * M%:num]] (g x) by exists x.
   move/gL3=> ->; rewrite !mulNr opprK; apply/andP; split.
-    by rewrite -lerBlDr -opprD -2!mulrDl natr1 divrr ?unitfE// mul1r.
+    by rewrite -lerBlDr -opprD -2!mulrDl natr1 divff// mul1r.
   rewrite -lerBrDr -2!mulrBl -(@natrB _ 2 1)// (le_trans xL)//.
   by rewrite ler_pM2r// ltW// gtrN// divr_gt0.
 have [xR|xR] := lerP (1/3 * M%:num) (f x).
@@ -584,7 +584,7 @@ have [xR|xR] := lerP (1/3 * M%:num) (f x).
   move/gR3 => ->; apply/andP; split.
     rewrite lerBrDl -2!mulrBl (le_trans _ xR)// ler_pM2r//.
     by rewrite ler_wpM2r ?invr_ge0 ?ler0n// lerBlDl natr1 ler1n.
-  by rewrite lerBlDl -2!mulrDl nat1r divrr ?mul1r// unitfE.
+  by rewrite lerBlDl -2!mulrDl nat1r divff ?mul1r.
 have /andP[ng3 pg3] : -(1/3) * M%:num <= g x <= 1/3 * M%:num.
   by apply: grng; exists x.
 rewrite ?(intrD _ 1 1) !mulrDl; apply/andP; split.
@@ -606,7 +606,7 @@ by move=> bd pm cf; have [g ?] := tietze_step' pm cf bd; exists g.
 Qed.
 
 Let onem_twothirds : 1 - 2/3 = 1/3 :> R.
-Proof. by apply/eqP; rewrite subr_eq/= -mulrDl nat1r divrr// unitfE. Qed.
+Proof. by apply/eqP; rewrite subr_eq/= -mulrDl nat1r divff. Qed.
 
 (** Tietze's theorem: *)
 Lemma continuous_bounded_extension (f : X -> R^o) M :
@@ -681,7 +681,7 @@ exists (lim (h_ @ \oo)); split.
   rewrite (le_trans (lim_series_norm _))//; apply: le_trans.
     exact/(lim_series_le cvg_gt _ (g_bd ^~ t))/is_cvg_geometric_series.
   rewrite (cvg_lim _ (cvg_geometric_series _))//; last exact: Rhausdorff.
-  by rewrite onem_twothirds mulrAC divrr ?mul1r// unitfE.
+  by rewrite onem_twothirds mulrAC divff mul1r.
 Unshelve. all: by end_near. Qed.
 
 End Tietze.
diff --git a/theories/probability.v b/theories/probability.v
@@ -745,7 +745,7 @@ rewrite eqr_div; [|apply: lt0r_neq0..]; last 2 first.
 - by rewrite exprz_gt0 -1?[ltLHS]addr0 ?ltr_leD.
 - by rewrite ltr_wpDl ?fine_ge0 ?variance_ge0 ?exprz_gt0.
 apply/eqP; have -> : fine 'V_P[X] = (u0 * lambda)%R.
-  by rewrite /u0 -mulrA mulVr ?mulr1 ?unitfE ?gt_eqF.
+  by rewrite /u0 -mulrA mulVf ?mulr1 ?gt_eqF.
 by rewrite -mulrDl -mulrDr (addrC u0) [in RHS](mulrAC u0) -exprnP expr2 !mulrA.
 Qed.
 
diff --git a/theories/sequences.v b/theories/sequences.v
@@ -825,7 +825,7 @@ suff abel : forall n,
     set h := 'o_\oo (@harmonic R).
     apply/eqoP => _/posnumP[e] /=.
     near=> n; rewrite normr1 mulr1 normrM -ler_pdivlMl ?normr_gt0//.
-    rewrite mulrC -normrV ?unitfE //.
+    rewrite mulrC -normfV.
     near: n.
     by case: (eqoP eventually_filterType (@harmonic R) h) => Hh _; apply Hh.
   move: (cesaro a_o); rewrite /arithmetic_mean /series /= -/a_.
@@ -836,7 +836,7 @@ case => [|n].
 rewrite /arithmetic_mean /= seriesEnat /= big_nat_recl //=.
 under eq_bigr do rewrite [u_ _]eq_sum_telescope.
 rewrite big_split /= big_const_nat iter_addr addr0 addrA -mulrS mulrDr.
-rewrite -(mulr_natl (u_ O)) mulrA mulVr ?unitfE ?pnatr_eq0 // mul1r opprD addrA.
+rewrite -(mulr_natl (u_ O)) mulrA mulVf ?pnatr_eq0// mul1r opprD addrA.
 rewrite eq_sum_telescope (addrC (u_ O)) addrK.
 rewrite [X in _ - _ * X](_ : _ =
     \sum_(0 <= i < n.+1) \sum_(0 <= k < n.+1 | (k < i.+1)%N) a_ k); last first.
@@ -863,7 +863,7 @@ rewrite [X in _ - _ * X](_ : _ =
 rewrite big_distrr /= big_mkord (big_morph _ (@opprD _) (@oppr0 _)).
 rewrite seriesEord -big_split /= big_add1 /= big_mkord; apply: eq_bigr => i _.
 rewrite mulrCA -[X in X - _]mulr1 -mulrBr [RHS]mulrC; congr (_ * _).
-rewrite -[X in X - _](@divrr _ (n.+2)%:R) ?unitfE ?pnatr_eq0 //.
+rewrite -[X in X - _](@divff _ (n.+2)%:R) ?pnatr_eq0//.
 rewrite [in X in _ - X]mulrC -mulrBl; congr (_ / _).
 rewrite -natrB; last by rewrite (@leq_trans n.+1) // leq_subr.
 rewrite subnBA; by [rewrite addSnnS addnC addnK | rewrite ltnW].
@@ -966,8 +966,7 @@ rewrite (_ : series _ = series (geometric (r / (2 ^ n.+1)%:R) 2^-1%R)); last fir
   rewrite funeqE => m; rewrite /series /=; apply: eq_bigr => k _.
   by rewrite expnD natrM (mulrC (2 ^ k)%:R) invfM exprVn (natrX _ 2 k) mulrA.
 apply: cvg_trans.
-  apply: cvg_geometric_series.
-  by rewrite ger0_norm // invr_lt1 // ?ltr1n // unitfE.
+  by apply: cvg_geometric_series; rewrite ger0_norm // invf_lt1 // ?ltr1n.
 rewrite [X in (X - _)%R](splitr 1) div1r addrK.
 by rewrite -mulrA -invfM expnSr natrM -mulrA divff// mulr1 natrX.
 Qed.
@@ -2634,7 +2633,7 @@ have /le_trans -> // : `| y n - y (n + m)| <=
   rewrite -[q%:num]/(q'%:num) -!mulrA -mulrDr ler_pM// {}/q'/=.
   rewrite -!/(`1-_) -mulrDr exprSr onemM -addrA.
   rewrite -[in leRHS](mulrC _ `1-(_ ^+ m)) -onemMr onemK.
-  by rewrite [in leRHS]mulrDl mulrAC mulrV ?mul1r// unitf_gt0// onem_gt0.
+  by rewrite [in leRHS]mulrDl mulrAC mulfV ?mul1r// gt_eqF// onem_gt0.
 rewrite geometric_seriesE ?lt_eqF//= -[leRHS]mulr1 (ACl (1*4*2*3))/= -/C.
 by rewrite ler_wpM2l// 1?mulr_ge0// lerBlDr lerDl.
 Qed.
