rm warnings, minor fix

affeldt-aist · Oct 2, 2023 · 2e6e0a5 · 2e6e0a5
1 parent 6479e50
commit 2e6e0a5
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 8 deletions.
diff --git a/theories/exp.v b/theories/exp.v
@@ -793,7 +793,7 @@ rewrite le_eqVlt => /predU1P[<- b0 p0 q0 _|a0].
 rewrite le_eqVlt => /predU1P[<-|b0] p0 q0 pq.
   by rewrite mulr0 powR0 ?gt_eqF// mul0r addr0 divr_ge0 ?powR_ge0 ?ltW.
 have q01 : (q^-1 \in `[0, 1])%R.
-  by rewrite in_itv/= invr_ge0 (ltW q0)/= -pq ler_paddl// invr_ge0 ltW.
+  by rewrite in_itv/= invr_ge0 (ltW q0)/= -pq ler_wpDl// invr_ge0 ltW.
 have ap0 : (0 < a `^ p)%R by rewrite powR_gt0.
 have bq0 : (0 < b `^ q)%R by rewrite powR_gt0.
 have := @concave_ln _ (@Itv.mk _ `[0, 1] _ q01)%R _ _ ap0 bq0.

diff --git a/theories/normedtype.v b/theories/normedtype.v
@@ -1203,7 +1203,7 @@ Proof.
 move=> /[apply] -[] _/posnumP[r] /subset_ball_prop_in_itv xrA.
 exists r%:num => //= k; rewrite /= distrC subr0 set_itvoo => /ltr_normlW kr k0.
 by apply/(subset_trans _ xrA)/subset_itvW;
-  [rewrite ler_sub//; exact: ltW | rewrite ler_add//; exact: ltW].
+  [rewrite lerB//; exact: ltW | rewrite lerD//; exact: ltW].
 Qed.
 
 Lemma open_itvcc_subset :
@@ -1214,8 +1214,8 @@ have -> : r%:num = 2 * (r%:num / 2) by rewrite mulrCA divff// mulr1.
 move/subset_ball_prop_in_itvcc => /= xrA; exists (r%:num / 2) => //= k.
 rewrite /= distrC subr0 set_itvcc => /ltr_normlW kr k0.
 move=> z /andP [xkz zxk]; apply: xrA => //; rewrite in_itv/=; apply/andP; split.
-  by rewrite (le_trans _ xkz)// ler_sub// ltW.
-by rewrite (le_trans zxk)// ler_add// ltW.
+  by rewrite (le_trans _ xkz)// lerB// ltW.
+by rewrite (le_trans zxk)// lerD// ltW.
 Qed.
 
 End open_itv_subset.

diff --git a/theories/reals.v b/theories/reals.v
@@ -329,16 +329,16 @@ move=> /[dup] supA [[a Aa] ubA] /[dup] supB [[b Bb] ubB].
 have ABsup : has_sup [set x + y | x in A & y in B].
   split; first by exists (a + b), a => //; exists b.
   case: ubA ubB => p up [q uq]; exists (p + q) => ? [r Ar [s Bs] <-].
-  by apply: ler_add; [exact: up | exact: uq].
+  by apply: lerD; [exact: up | exact: uq].
 apply: le_anti; apply/andP; split.
   apply: sup_le_ub; first by case: ABsup.
-  by move=> ? [p Ap [q Bq] <-]; apply: ler_add; exact: sup_ub.
+  by move=> ? [p Ap [q Bq] <-]; apply: lerD; exact: sup_ub.
 rewrite real_leNgt ?num_real// -subr_gt0; apply/negP.
 set eps := (_ + _ - _) => epos.
 have e2pos : 0 < eps / 2%:R by rewrite divr_gt0// ltr0n.
 have [r Ar supBr] := sup_adherent e2pos supA.
 have [s Bs supAs] := sup_adherent e2pos supB.
-have := ltr_add supBr supAs.
+have := ltrD supBr supAs.
 rewrite -addrA [-_+_]addrC -addrA -opprD -splitr addrA /= opprD opprK addrA.
 rewrite subrr add0r; apply/negP; rewrite -real_leNgt ?num_real//.
 by apply: sup_upper_bound => //; exists r => //; exists s.

diff --git a/theories/sequences.v b/theories/sequences.v
@@ -1473,7 +1473,7 @@ Proof. by rewrite fine_cvgP. Qed.
 Notation ereal_cvg_real := __deprecated__ereal_cvg_real.
 
 Lemma ereal_nondecreasing_cvg (R : realType) (u_ : (\bar R)^nat) :
-  nondecreasing_seq u_ -> u_ @ \oo --> ereal_sup (u_ @` setT).
+  nondecreasing_seq u_ -> u_ @ \oo --> ereal_sup (range u_).
 Proof.
 move=> nd_u_; set S := u_ @` setT; set l := ereal_sup S.
 have [Spoo|Spoo] := pselect (S +oo).