Adapt to MC#1256

CHANGELOG_UNRELEASED.md

@@ -161,6 +161,8 @@
 
 - in `classical_sets.v`:
   + lemmas `Zorn` and `ZL_preorder` now require a relation of type `rel T` instead of `T -> T -> Prop`
+- in `mathcomp_extra.v`:
+  + Notation "f \^-1" now at level 35 with f at next level
 
 ### Renamed
 

classical/mathcomp_extra.v

@@ -244,7 +244,7 @@ Proof. by move=> F0; elim/big_rec : _ => // i x Pi; apply/ler_wnDl/F0. Qed.
 Inductive boxed T := Box of T.
 
 Reserved Notation "`1- r" (format "`1- r", at level 2).
-Reserved Notation "f \^-1" (at level 3, format "f \^-1", left associativity).
+Reserved Notation "f \^-1" (at level 35, format "f \^-1").
 
 (* TODO: To be backported to finmap *)
 

theories/altreals/realseq.v

@@ -213,7 +213,7 @@ apply/asboolP/nboundedP; exists e => [|n]; first by rewrite lt_max ltr_wpDl.
 case: (ltnP n K); last first.
   move/cu; rewrite inE eclamp_id ?ltr01 // => ltunBx1.
   rewrite lt_max; apply/orP; left; rewrite -[u n](addrK x) addrAC.
-  by apply/(le_lt_trans (ler_normD _ _)); rewrite addrC ltrD2l.
+  by apply/(le_lt_trans (ler_normD _ _)); rewrite [ltLHS]addrC ltrD2l.
 move=> lt_nK; have: `|u n| \in S; first by apply/map_f; rewrite mem_iota.
 move=> un_S; rewrite lt_max; apply/orP; right.
 case E: {+}K lt_nK => [|k] // lt_nSk; apply/ltr_pwDr; first apply/ltr01.

theories/derive.v

@@ -721,7 +721,7 @@ Fact dcomp (U V' W' : normedModType R) (f : U -> V') (g : V' -> W') x :
 Proof.
 move=> df dg; split; first by move=> ?; apply: continuous_comp.
 apply: eqaddoEx => y; rewrite diff_locallyx// -addrA diff_locallyxC// linearD.
-rewrite addrA -addrA; congr (_ + _ + _).
+rewrite addrA -[LHS]addrA; congr (_ + _ + _).
 rewrite diff_eqO // ['d f x : _ -> _]diff_eqO //.
 by rewrite {2}eqoO addOx compOo_eqox compoO_eqox addox.
 Qed.

theories/esum.v

@@ -273,7 +273,7 @@ apply lee_fsum=> [|i Xi]; first exact: finite_set_fst.
 rewrite ereal_sup_ubound //=; have ? : finite_set (X.`2 `&` J i).
   by apply: finite_setI; left; exact: finite_set_snd.
 exists (X.`2 `&` J i) => //.
-rewrite [in RHS]big_fset_condE/= fsbig_finite//; apply eq_fbigl => j.
+rewrite [in RHS]big_fset_condE/= fsbig_finite//; apply/eq_fbigl => j.
 by rewrite in_fset_set// !inE/= in_setI in_fset_set//; exact: finite_set_snd.
 Qed.
 

theories/lebesgue_integral.v

@@ -5989,7 +5989,7 @@ move: a0; rewrite le_eqVlt => /predU1P[a0|a0].
   move=> y; rewrite /ball/= => xyd.
   have ? : ball x r `<=` ball y (r + d).
     move=> /= z; rewrite /ball/= => xzr; rewrite -(subrK x y) -(addrA (y - x)%R).
-    by rewrite (le_lt_trans (ler_normD _ _))// addrC ltrD// distrC.
+    by rewrite (le_lt_trans (ler_normD _ _))// [ltLHS]addrC ltrD// distrC.
   have ? : k <= \int[mu]_(y in ball y (r + d)) `|(f y)%:E|.
     apply: ge0_subset_integral =>//; [exact:measurable_ball|
                                       exact:measurable_ball|].
@@ -6027,7 +6027,7 @@ exists (ball x d).
 move=> y; rewrite /ball/= => xyd.
 have ? : ball x r `<=` ball y (r + d).
   move=> /= z; rewrite /ball/= => xzr; rewrite -(subrK x y) -(addrA (y - x)%R).
-  by rewrite (le_lt_trans (ler_normD _ _))// addrC ltrD// distrC.
+  by rewrite (le_lt_trans (ler_normD _ _))// [ltLHS]addrC ltrD// distrC.
 have ? : k <= \int[mu]_(z in ball y (r + d)) `|(f z)%:E|.
   apply: ge0_subset_integral => //; [exact: measurable_ball|
                                      exact: measurable_ball|].

theories/topology.v

@@ -5845,7 +5845,7 @@ move: e1 e2 x z; elim: n.
     - apply: n_step_ball_le; last exact: Oxy.
       by rewrite -deE lerDl; apply: ltW.
     - apply: (@n_step_ball_le _ _ d2); last by split.
-      rewrite -[e2]addr0 -(subrr e1) addrA -lerBlDr opprK addrC.
+      rewrite -[e2]addr0 -(subrr e1) addrA -lerBlDr opprK [leLHS]addrC.
       by rewrite [e2 + _]addrC -deE; exact: lerD.
     - by rewrite addn0.
   move=> /negP; rewrite -ltNge//.