Fixes compatibility with SSReflect 1.16.0

math-comp · Oct 3, 2023 · 2a88a17 · 2a88a17
1 parent 5211206
commit 2a88a17
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/theories/hoelder.v b/theories/hoelder.v
@@ -291,7 +291,7 @@ Local Open Scope ring_scope.
 
 Lemma lerBr (x y : R) : (0 <= y -> x - y <= x)%R.
 Proof.
-by move=> x0; rewrite lerBlDl ler_addr.
+by move=> x0; rewrite -(subr0 x) ler_sub ?subr0.
 Qed.
 
 Lemma convex_powR p : 1 <= p ->
@@ -451,7 +451,7 @@ rewrite le_eqVlt => /orP [/eqP <-|p1].
   - by repeat apply: measurableT_comp => //; apply: measurable_funD.
   - apply: measurableT_comp => //.
     by apply: measurable_funD; apply: measurableT_comp.
-  - by move=> x _; rewrite lee_fin ler_normD.
+  - by move=> x _; rewrite lee_fin ler_norm_add.
   by rewrite le_eqVlt ge0_integralD ?eqxx//; repeat apply: measurableT_comp => //.  
 have [->|Nfoo] := eqVneq 'N_p%:E[f] +oo.
   by rewrite addye ?leey// -ltNye (lt_le_trans _ (Lnorm_ge0 _ _ _)).