From 2ab529bc13298333befba2d321118ab4ecf4f802 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Mon, 22 Jan 2024 13:24:18 +0900
Subject: [PATCH] fix

- to the precedeing merge remote-tracking branch
  'origin/hierarchy-builder'
---
 README.md             |  4 ----
 theories/normedtype.v | 10 +++++-----
 theories/sequences.v  | 10 +++++-----
 3 files changed, 10 insertions(+), 14 deletions(-)

diff --git a/README.md b/README.md
index a35cba041..e669c9de9 100644
--- a/README.md
+++ b/README.md
@@ -33,11 +33,7 @@ the Coq proof-assistant and using the Mathematical Components library.
   - Pierre-Yves Strub (initial)
   - Laurent Théry
 - License: [CeCILL-C](LICENSE)
-<<<<<<< HEAD
 - Compatible Coq versions: Coq 8.15 to 8.18 (or dev)
-=======
-- Compatible Coq versions: Coq 8.14 to 8.18 (or dev)
->>>>>>> origin/hierarchy-builder
 - Additional dependencies:
   - [MathComp ssreflect 1.17 or later](https://math-comp.github.io)
   - [MathComp fingroup 1.17 or later](https://math-comp.github.io)
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 63bd2b213..b3e4686da 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -1312,7 +1312,7 @@ Proof.
 move=> pPf e; apply: contrapT => /forallPNP pePf; apply: pPf; near=> t.
 apply: contrapT; apply: pePf; apply/andP; split.
 - by near: t; exact: nbhs_right_gt.
-- by near: t; apply: nbhs_right_lt; rewrite ltr_addl.
+- by near: t; apply: nbhs_right_lt; rewrite ltrDl.
 Unshelve. all: by end_near. Qed.
 
 Lemma withinN (A : set R) a :
@@ -1336,14 +1336,14 @@ Lemma at_rightN a : (- a)^'+ = -%R @ a^'-.
 Proof.
 rewrite /at_right withinN [X in within X _](_ : _ = [set u | u < a])//.
 rewrite (@fun_predC _ -%R)/=; last exact: opprK.
-by rewrite image_id; under eq_fun do rewrite ltr_oppl opprK.
+by rewrite image_id; under eq_fun do rewrite ltrNl opprK.
 Qed.
 
 Lemma at_leftN a : (- a)^'- = -%R @ a^'+.
 Proof.
 rewrite /at_left withinN [X in within X _](_ : _ = [set u | a < u])//.
 rewrite (@fun_predC _ -%R)/=; last exact: opprK.
-by rewrite image_id; under eq_fun do rewrite ltr_oppl opprK.
+by rewrite image_id; under eq_fun do rewrite ltrNl opprK.
 Qed.
 
 End at_left_right.
@@ -2094,13 +2094,13 @@ move=> ab; split=> [abf|].
     rewrite -nbhs_subspace_in// /within/= near_simpl.
     apply: filter_app; exists (b - a); rewrite /= ?subr_gt0// => c cba + ac.
     apply=> //; rewrite ?gt_eqF// !in_itv/= (ltW ac)/=; move: cba => /=.
-    by rewrite ltr0_norm ?subr_lt0// opprB ltr_add2r => /ltW.
+    by rewrite ltr0_norm ?subr_lt0// opprB ltrD2r => /ltW.
   + move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf b).
     rewrite /dnbhs/= near_withinE !near_simpl /prop_near1 /nbhs/=.
     rewrite -nbhs_subspace_in// /within/= near_simpl.
     apply: filter_app; exists (b - a); rewrite /= ?subr_gt0// => c cba + ac.
     apply=> //; rewrite ?lt_eqF// !in_itv/= (ltW ac)/= andbT; move: cba => /=.
-    by rewrite gtr0_norm ?subr_gt0// ltr_add2l ltr_oppr opprK => /ltW.
+    by rewrite gtr0_norm ?subr_gt0// ltrD2l ltrNr opprK => /ltW.
 case=> ctsoo [ctsL ctsR]; apply/subspace_continuousP => x /andP[].
 rewrite !bnd_simp/= !le_eqVlt => /predU1P[<-{x}|ax] /predU1P[|].
 - by move/eqP; rewrite lt_eqF.
diff --git a/theories/sequences.v b/theories/sequences.v
index c79353dc7..5f70e5e64 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -2453,14 +2453,14 @@ move=> ba bb; have ab k : infs u k + infs v k <= infs (u \+ v) k.
   by move=> M [n /= kn <-]; apply: lerD; apply: inf_lb; [
     exact/has_lbound_sdrop/bounded_fun_has_lbound; exact | exists n |
     exact/has_lbound_sdrop/bounded_fun_has_lbound; exact | exists n ].
-have cu : cvg (infs u).
+have cu : cvgn (infs u).
   apply: nondecreasing_is_cvgn; last exact: bounded_fun_has_ubound_infs.
   exact/nondecreasing_infs/bounded_fun_has_lbound.
-have cv : cvg (infs v).
+have cv : cvgn (infs v).
   apply: nondecreasing_is_cvgn; last exact: bounded_fun_has_ubound_infs.
   exact/nondecreasing_infs/bounded_fun_has_lbound.
-rewrite -(@limD _ [normedModType R of R^o] _ _ _ _ _ cu cv); apply: ler_lim.
-- exact: (@is_cvgD _ [normedModType R of R^o] _ _ _ _ _ cu cv).
+rewrite -(limD cu cv); apply: ler_lim.
+- exact: is_cvgD cu cv.
 - apply: nondecreasing_is_cvgn; last first.
     exact/bounded_fun_has_ubound_infs/bounded_funD.
   exact/nondecreasing_infs/bounded_fun_has_lbound/bounded_funD.
@@ -2862,7 +2862,7 @@ have [q_gt0 | | q0] := ltrgt0P q%:num.
 - near=> n => /=; apply: (le_lt_trans (@ctrfq (_, _) _)) => //=.
   + split; last exact: funS.
     by apply: closed_cvg contraction_cvg => //; apply: nearW => ?; exact: funS.
-  + rewrite -ltr_pdivl_mull //; near: n; move/cvgrPdist_lt: contraction_cvg.
+  + rewrite -ltr_pdivlMl //; near: n; move/cvgrPdist_lt: contraction_cvg.
     by apply; rewrite mulr_gt0 // invr_gt0.
 - by rewrite ltNge//; exact: contraNP.
 - apply: nearW => /= n; apply: (le_lt_trans (@ctrfq (_, _) _)).