diff --git a/CaseStudies/Convergence/Algorithm_noB.v b/CaseStudies/Convergence/Algorithm_noB.v
index cdc2905d87a5f96ee6869ed063c9e8b6b01aa016..a089825fc78b0f05efa00e53b4d29ff4bb5b1772 100644
--- a/CaseStudies/Convergence/Algorithm_noB.v
+++ b/CaseStudies/Convergence/Algorithm_noB.v
@@ -18,9 +18,19 @@
 (**************************************************************************)
 
 
-Require Import Utf8 Reals SetoidDec Lia SetoidList.
-From Pactole Require Import Util.Preliminary Util.Fin Setting Spaces.R2
-  Observations.SetObservation Models.Rigid Models.NoByzantine Models.Similarity.
+Require Import Utf8.
+Require Import Reals.
+Require Import SetoidDec.
+Require Import Lia.
+Require Import SetoidList.
+Require Import Pactole.Util.Preliminary.
+Require Import Pactole.Util.Fin.
+Require Import Pactole.Setting.
+Require Import Pactole.Spaces.R2.
+Require Import Pactole.Observations.SetObservation.
+Require Import Pactole.Models.Rigid.
+Require Import Pactole.Models.NoByzantine.
+Require Import Pactole.Models.Similarity.
 Set Implicit Arguments.
 Close Scope R_scope.
 Import Datatypes.
diff --git a/CaseStudies/Convergence/Impossibility_2G_1B.v b/CaseStudies/Convergence/Impossibility_2G_1B.v
index 5ee361a8755045a88670a54b83a97833a47a64e8..ed342e7681d536784c5514533b7589c34cda1107 100644
--- a/CaseStudies/Convergence/Impossibility_2G_1B.v
+++ b/CaseStudies/Convergence/Impossibility_2G_1B.v
@@ -18,9 +18,21 @@
 (**************************************************************************)
 
 
-Require Import Utf8 Reals Psatz SetoidDec Arith.Div2 Lia SetoidList.
-From Pactole Require Import Util.Preliminary Util.Fin Util.Enum Setting Spaces.R
-  Observations.MultisetObservation Models.Similarity Models.Rigid.
+Require Import Utf8.
+Require Import Reals.
+Require Import Psatz.
+Require Import SetoidDec.
+Require Import Arith.Div2.
+Require Import Lia.
+Require Import SetoidList.
+Require Import Pactole.Util.Preliminary.
+Require Import Pactole.Util.Fin.
+Require Import Pactole.Util.Enum.
+Require Import Pactole.Setting.
+Require Import Pactole.Spaces.R.
+Require Import Pactole.Observations.MultisetObservation.
+Require Import Pactole.Models.Similarity.
+Require Import Pactole.Models.Rigid.
 Set Implicit Arguments.
 Close Scope R_scope.
 Close Scope VectorSpace_scope.
@@ -122,7 +134,7 @@ Proof using n_non_0.
 assert (Hn0 := n_non_0). rewrite nG_nB, nB_value.
 destruct n as [| ?].
 - lia.
-- simpl. rewrite plus_comm. simpl. lia.
+- cbn. rewrite Nat.add_comm. cbn. lia.
 Qed.
 
 (* TODO: move to a definition/problem file *)
@@ -231,7 +243,7 @@ Lemma glast_right : In glast right.
 Proof using .
 rewrite right_spec. simpl. assert (Heven := even_nG).
 destruct n as [| [| ]]; simpl; auto; [].
-apply le_n_S, Nat.div2_decr, le_n_Sn.
+apply le_n_S, Nat.div2_decr, Nat.le_succ_diag_r.
 Qed.
 
 Hint Resolve gfirst_left glast_right left_right_exclusive : core.
diff --git a/CaseStudies/Exploration/ImpossibilityKDividesN.v b/CaseStudies/Exploration/ImpossibilityKDividesN.v
index 9ba8b338f923f2d5611e339694b069a37d8119f0..b1bbb07fe82bb7b3adda52f562ad4017b0ce904d 100644
--- a/CaseStudies/Exploration/ImpossibilityKDividesN.v
+++ b/CaseStudies/Exploration/ImpossibilityKDividesN.v
@@ -7,9 +7,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
-Require Import Utf8 Arith SetoidList.
-From Pactole Require Import Util.Stream Models.NoByzantine
-  Models.RingSSync CaseStudies.Exploration.ExplorationDefs.
+Require Import Utf8.
+Require Import Arith.
+Require Import SetoidList.
+Require Import Pactole.Util.Stream.
+Require Import Pactole.Models.NoByzantine.
+Require Import Pactole.Models.RingSSync.
+Require Import Pactole.CaseStudies.Exploration.ExplorationDefs.
 
 Set Implicit Arguments.
 Typeclasses eauto := (bfs).
diff --git a/CaseStudies/Exploration/Tower.v b/CaseStudies/Exploration/Tower.v
index b3f163219c87c39e0e3fcc23af6c6164ef54059c..78a5ad6ef6043d8ed2ec7c0bb6dc3cb0842dfdf2 100644
--- a/CaseStudies/Exploration/Tower.v
+++ b/CaseStudies/Exploration/Tower.v
@@ -16,9 +16,15 @@
                                                                           *)
 (**************************************************************************)
 
-Require Import Utf8 SetoidList Arith_base Lia.
-From Pactole Require Import Util.Stream Util.Enum Util.Fin Models.NoByzantine
-  Models.RingSSync CaseStudies.Exploration.ExplorationDefs.
+Require Import Utf8.
+Require Import List SetoidList.
+Require Import Arith_base Lia.
+Require Import Pactole.Util.Stream.
+Require Import Pactole.Util.Enum.
+Require Import Pactole.Util.Fin.
+Require Import Pactole.Models.NoByzantine.
+Require Import Pactole.Models.RingSSync.
+Require Import Pactole.CaseStudies.Exploration.ExplorationDefs.
 
 Open Scope list_scope.
 Set Implicit Arguments.
diff --git a/Spaces/R.v b/Spaces/R.v
index 80d7c738e69f755711ec49122e39ae8a80e9ebab..3a8897342690b722f055abdb044fe3956fb400b5 100644
--- a/Spaces/R.v
+++ b/Spaces/R.v
@@ -412,7 +412,7 @@ intro sim. destruct (similarity_in_R_case sim) as [Hinc | Hdec].
   apply similarity_decreasing; trivial; [].
   (* TODO Coq 8.17 : does [lra] work again? *)
   rewrite <- (Rplus_opp_r (zoom sim)), <- Rminus_0_l.
-  unfold Rminus. apply Rplus_le_compat; try reflexivity; []. apply Rlt_le, zoom_pos.
+  unfold Rminus. apply Rplus_le_compat; try lra; []. apply Rlt_le, zoom_pos.
 Qed.
 
 (** To conclude that two similarities are equal, it is enough to show that they are equal on two points. *)