diff --git a/CaseStudies/Convergence/Impossibility_2G_1B.v b/CaseStudies/Convergence/Impossibility_2G_1B.v
index f6ccd820ae267b7872dee2f6b390221278464d28..648748d9d4420ae7bc4c21bc7071fb69cc91cb34 100644
--- a/CaseStudies/Convergence/Impossibility_2G_1B.v
+++ b/CaseStudies/Convergence/Impossibility_2G_1B.v
@@ -608,7 +608,7 @@ induction Hpt as [e IHpt | e IHpt]; intros start Hstart.
   clear -absurdmove Hnow1 Hnow2 n_non_0. specialize (Hnow1 gfirst). specialize (Hnow2 gfirst).
   cut (Rabs move <= Rabs (move / 3) + Rabs (move / 3)).
   - assert (Hpos : 0 < Rabs move) by now apply Rabs_pos_lt.
-    unfold Rdiv. rewrite Rabs_mult, Rabs_Rinv; try lra.
+    unfold Rdiv. rewrite Rabs_mult, Rabs_inv; try lra.
     assert (Habs3 : Rabs 3 = 3). { apply Rabs_pos_eq. lra. } rewrite Habs3 in *.
     lra.
   - simpl in *. rewrite sqrt_square in Hnow1, Hnow2.
diff --git a/CaseStudies/Exploration/ImpossibilityKDividesN.v b/CaseStudies/Exploration/ImpossibilityKDividesN.v
index 2c92553f0eba12a31e5e79912813db8ee941351a..0a0269cf42aa284c7d33c79b6444cc8a337a27d7 100644
--- a/CaseStudies/Exploration/ImpossibilityKDividesN.v
+++ b/CaseStudies/Exploration/ImpossibilityKDividesN.v
@@ -30,14 +30,14 @@ Hypothesis kdn : (n mod k = 0).
 Hypothesis k_inf_n : (k < n).
 
 Lemma h_not_0: n <> 0.
-Proof.
+Proof using ltc_2_n.
   unfold ltc in *.
   apply neq_lt. 
   transitivity 2; auto with arith.
 Qed.
 
 Lemma k_not_0: k <> 0.
-Proof.
+Proof using ltc_0_k.
   unfold ltc in *.
   now apply neq_lt. 
 Qed.
@@ -45,7 +45,7 @@ Qed.
 Local Hint Resolve h_not_0 k_not_0: localDB.
 
 Lemma local_subproof1 : n = k * (n / k).
-Proof using kdn ltc_0_k. apply Nat.div_exact. auto with localDB. auto with localDB. Qed.
+Proof using kdn ltc_0_k. apply Nat.Div0.div_exact. auto with localDB. Qed.
 
 Lemma local_subproof2 : n / k ≠ 0.
 Proof using kdn ltc_2_n ltc_0_k.
@@ -126,26 +126,26 @@ Proof using kdn ltc_0_k k_inf_n.
       exists (Good id'). split. 2:{ rewrite InA_Leibniz. apply In_names. }
       rewrite <- Hpt. cbn -[create_ref_config BijectionInverse]. split; trivial; [].
       change G with (fin k) in *. unfold create_ref_config, Datatypes.id, id'. apply fin2natI.
-      rewrite 2 subf2nat, 3 mod2fin2nat, Nat.add_mod_idemp_l, 2 (Nat.mod_small (_ * _));auto with localDB.
+      rewrite 2 subf2nat, 3 mod2fin2nat, Nat.Div0.add_mod_idemp_l, 2 (Nat.mod_small (_ * _));auto with localDB.
       - pattern n at 3 5. rewrite local_subproof1.
         rewrite <- Nat.mul_sub_distr_r, <- Nat.mul_add_distr_r.
-        rewrite Nat.mul_mod_distr_r;try auto with localDB.
+        rewrite Nat.Div0.mul_mod_distr_r;try auto with localDB.
       - apply local_subproof3, fin_lt.
       - pattern n at 2. rewrite local_subproof1, <- Nat.mul_lt_mono_pos_r; try apply mod2fin_lt; [].
         apply Nat.neq_0_lt_0, local_subproof2.
     + pose (id' := addf g' g). change (fin k) with G in id'.
       exists (Good id'). split. 2:{ rewrite InA_Leibniz. apply In_names. }
       rewrite <- Hpt. cbn. split. 2: reflexivity. unfold create_ref_config, id', Datatypes.id. apply fin2natI.
-      rewrite subf2nat, 3 mod2fin2nat, addf2nat, Nat.add_mod_idemp_l, 2 (Nat.mod_small (_ * _));
+      rewrite subf2nat, 3 mod2fin2nat, addf2nat, Nat.Div0.add_mod_idemp_l, 2 (Nat.mod_small (_ * _));
       try (pattern n at 2; rewrite local_subproof1, <- Nat.mul_lt_mono_pos_r; try apply fin_lt;           
            [];
            apply Nat.div_str_pos; split; trivial; []; now apply Nat.lt_le_incl); try lia ;[].
       rewrite local_subproof1 at 2 4.
-      rewrite <- Nat.mul_sub_distr_r, <- Nat.mul_add_distr_r, Nat.mul_mod_distr_r; auto with localDB.
+      rewrite <- Nat.mul_sub_distr_r, <- Nat.mul_add_distr_r, Nat.Div0.mul_mod_distr_r; auto with localDB.
       apply Nat.mul_cancel_r; try apply local_subproof2; [].
-      rewrite Nat.add_mod_idemp_l, <- Nat.add_assoc, (Nat.add_comm (fin2nat g)), Nat.sub_add;
+      rewrite Nat.Div0.add_mod_idemp_l, <- Nat.add_assoc, (Nat.add_comm (fin2nat g)), Nat.sub_add;
       try apply Nat.lt_le_incl, fin_lt;auto with localDB.
-      rewrite <- Nat.add_mod_idemp_r, Nat.mod_same, Nat.add_0_r;auto with localDB. apply Nat.mod_small, fin_lt.
+      rewrite <- Nat.Div0.add_mod_idemp_r, Nat.Div0.mod_same, Nat.add_0_r;auto with localDB. apply Nat.mod_small, fin_lt.
 Qed.
 
 (** The demon activate all robots and shifts their view to be on 0. *)
@@ -210,13 +210,13 @@ Proof using Hmove kdn k_inf_n ltc_0_k.
   * rewrite Heq_e in Hvisited. cbn in Hvisited.
     apply (f_equal (@fin2nat n)) in Hvisited. revert Hvisited.
     cbn-[Nat.modulo Nat.div]. rewrite local_subproof1 at 2.
-    rewrite Nat.mul_mod_distr_r, (Nat.mod_small 1), Nat.mul_eq_1.
+    rewrite Nat.Div0.mul_mod_distr_r, (Nat.mod_small 1), Nat.mul_eq_1.
     intros [_ Habs].
     apply Nat.lt_nge in k_inf_n.
     contradiction k_inf_n.
     rewrite local_subproof1,
-    Habs, Nat.mul_1_r. reflexivity. 3: apply local_subproof2.
-    2: apply neq_u_l. eapply @lt_l_u. apply lt_s_u. auto.
+    Habs, Nat.mul_1_r. reflexivity.
+    eapply @lt_l_u. apply lt_s_u. auto.
   * apply IHvisited. rewrite Heq_e, execute_tail. rewrite round_id. f_equiv.
 Qed.
 
@@ -253,7 +253,7 @@ Lemma f_config_merge : ∀ config m1 m2,
 Proof using k_inf_n kdn.
   intros. unfold f_config. rewrite map_config_merge; autoclass; [].
   intros id. cbn-[equiv]. rewrite 3 asbmE, <- (addm_mod (config id)), <- mod2fin2nat,
-  <- addmA, addm2nat, mod2fin2nat, Nat.add_mod_idemp_l;auto with localDB.
+  <- addmA, addm2nat, mod2fin2nat, Nat.Div0.add_mod_idemp_l;auto with localDB.
   apply addm_mod.
 Qed.
 
@@ -303,7 +303,7 @@ Lemma equiv_config_m_sym : ∀ m config1 config2,
   -> equiv_config_m (@oppm 2 n ltc_2_n m) config2 config1.
 Proof using k_inf_n kdn.
   unfold equiv_config_m. intros * Hequiv. unshelve erewrite Hequiv,
-  f_config_merge, <- f_config_modulo, (proj2 (Nat.mod_divide _ _ _));auto with localDB.
+  f_config_merge, <- f_config_modulo, (proj2 (Nat.Lcm0.mod_divide _ _));auto with localDB.
   symmetry. apply f_config_0. apply divide_addn_oppm.
 Qed.
 
diff --git a/Makefile.local b/Makefile.local
index 0dc2b56c229a095ed6bdcacd2aa52a372d0de584..35c1d6bf68c70f9582e0935d89f1754b65b65684 100644
--- a/Makefile.local
+++ b/Makefile.local
@@ -33,6 +33,14 @@ vok-nocheck: $(VOKFILESNOASSUMPTION)
 # developpers could use this.
 # COQEXTRAFLAGS+= -set "Suggest Proof Using=yes" -w -deprecated-instance-without-locality
 
+COQEXTRAFLAGS+= -set "Suggest Proof Using=yes"
+COQEXTRAFLAGS+= -w -deprecated-instance-without-locality
+#COQEXTRAFLAGS+= -w -intuition-auto-with-star
+#COQEXTRAFLAGS+= -w -argument-scope-delimiter
+#COQEXTRAFLAGS+= -w -deprecated-syntactic-definition
+#COQEXTRAFLAGS+= -w -future-coercion-class-field
+
+
 core: Pactole_all.vo
 
 recore:
diff --git a/Spaces/R2.v b/Spaces/R2.v
index 109a957d3c4f37dae769bae2c53748fbc0cb1ff8..6eff916ba6e9e3c560101f449d2f516e7b7f6f21 100644
--- a/Spaces/R2.v
+++ b/Spaces/R2.v
@@ -965,7 +965,7 @@ destruct (Rlt_le_dec k kh) as [Hlt | Hle].
   right. ring.
   left. apply Rle_lt_trans with (r2 := k). tauto.
   assumption.
-  left. apply Rlt_Rminus. assumption.
+  left. apply Rlt_0_minus. assumption.
 
   destruct A, B; compute; f_equal; ring.
   destruct A, B; compute; f_equal; ring.
diff --git a/Spaces/RealMetricSpace.v b/Spaces/RealMetricSpace.v
index 4ded9998b5b4c1b0ff1ad0b47f8f41b30e43ffd4..7e5c1a03d24f7e78aa33db6412ec61e432699908 100644
--- a/Spaces/RealMetricSpace.v
+++ b/Spaces/RealMetricSpace.v
@@ -41,7 +41,7 @@ Lemma dist_nonneg `{RealMetricSpace} : forall u v, (0 <= dist u v)%R.
 Proof.
 intros x y. apply Rmult_le_reg_l with 2%R.
 + apply Rlt_R0_R2.
-+ do 2 rewrite double. rewrite Rplus_0_r.
++ do 2 rewrite <- Rplus_diag. rewrite Rplus_0_r.
   assert (Hx : equiv x x) by reflexivity. rewrite <- dist_defined in Hx. rewrite <- Hx.
   setoid_rewrite dist_sym at 3. apply triang_ineq.
 Qed.
diff --git a/Util/Fin.v b/Util/Fin.v
index bdce679ee4f97a2b8b103cd02b839630e96f16ff..db4773fadf371b29a8ce1bdf8a6f2403634068bb 100644
--- a/Util/Fin.v
+++ b/Util/Fin.v
@@ -182,7 +182,7 @@ Proof using . intros. reflexivity. Qed.
 
 Lemma mod2fin_mod : ∀ j : nat, mod2fin (j mod u) = mod2fin j.
 Proof using .
-  intros. apply fin2natI. rewrite 2 mod2fin2nat. apply Nat.mod_mod, neq_u_0.
+  intros. apply fin2natI. rewrite 2 mod2fin2nat. apply Nat.Div0.mod_mod.
 Qed.
 
 Lemma mod2fin_mod2fin : ∀ j : nat, mod2fin (mod2fin j) = mod2fin j.
@@ -212,7 +212,7 @@ Qed.
 Lemma mod2fin_muln : ∀ j : nat, mod2fin (u * j) = fin0.
 Proof using .
   intros. apply fin2natI. rewrite mod2fin2nat, fin02nat, Nat.mul_comm.
-  apply Nat.mod_mul, neq_u_0.
+  apply Nat.Div0.mod_mul.
 Qed.
 
 Lemma mod2fin_le_between_compat : ∀ p j1 j2 : nat, u * p <= j1 < u * p + u
@@ -233,20 +233,20 @@ Lemma addn_mod2fin_idemp_l : ∀ j1 j2 : nat,
   mod2fin (mod2fin j1 + j2) = mod2fin (j1 + j2).
 Proof using .
   intros. apply fin2natI. rewrite 3 mod2fin2nat.
-  apply Nat.add_mod_idemp_l, neq_u_0.
+  apply Nat.Div0.add_mod_idemp_l.
 Qed.
 
 Lemma addn_mod2fin_idemp_r : ∀ j1 j2 : nat,
   mod2fin (j1 + mod2fin j2) = mod2fin (j1 + j2).
 Proof using .
   intros. apply fin2natI. rewrite 3 mod2fin2nat.
-  apply Nat.add_mod_idemp_r, neq_u_0.
+  apply Nat.Div0.add_mod_idemp_r.
 Qed.
 
 Lemma divide_fin0_mod2fin : ∀ j : nat, Nat.divide u j -> mod2fin j = fin0.
 Proof using .
   intros * H. apply fin2natI. rewrite mod2fin2nat.
-  apply Nat.mod_divide, H. apply neq_u_0.
+  apply Nat.Lcm0.mod_divide, H.
 Qed.
 
 Lemma mod2fin0 : mod2fin 0 = fin0.
@@ -551,8 +551,8 @@ Qed.
 
 Lemma revm0 : revm 0 = fin_max.
 Proof using .
-  apply fin2natI. rewrite revm2nat, fin_max2nat, Nat.mod_0_l.
-  apply Nat.sub_0_r. apply neq_u_0.
+  apply fin2natI. rewrite revm2nat, fin_max2nat, Nat.Div0.mod_0_l.
+  apply Nat.sub_0_r.
 Qed.
 
 Lemma revf0 : revf fin0 = fin_max.
@@ -932,13 +932,26 @@ Lemma revf_addf : ∀ f1 f2 : fin u, revf (addf f1 f2) = subf (revf f1) f2.
 Proof using .
   intros. apply fin2natI. erewrite subf2nat, 2 revf2nat, addf2nat,
   Nat.add_sub_assoc, <- Nat.add_sub_swap, <- (Nat.mod_small (Nat.pred _ - _)),
-  <- Nat.sub_add_distr, <- (Nat.mod_add (_ - ((_ + _) mod _)) 1), Nat.mul_1_l,
-  <- Nat.add_sub_swap, (Nat.mod_eq (_ + _)), sub_sub,
-  (Nat.add_sub_swap _ (_ * _)), Nat.mul_comm, Nat.mod_add. reflexivity.
-  3: apply Nat.mul_div_le. 2: apply Nat.add_le_mono. 1,4,5,7: apply neq_u_0.
-  4: apply lt_sub_lt_add_l. 1,3,4,6: apply Nat.lt_le_pred.
-  6: apply Nat.lt_lt_add_l. 5,7: apply Nat.lt_le_incl. 1,4-6: apply fin_lt.
-  1,2: apply mod2fin_lt. all: apply lt_pred_u.
+  <- Nat.sub_add_distr, <- (Nat.Div0.mod_add (_ - ((_ + _) mod _)) 1), Nat.mul_1_l,
+  <- Nat.add_sub_swap, (Nat.Div0.mod_eq (_ + _)), sub_sub,
+  (Nat.add_sub_swap _ (_ * _)), Nat.mul_comm, Nat.Div0.mod_add. reflexivity.
+  - apply Nat.add_le_mono.
+    + apply Nat.lt_le_pred.
+      apply fin_lt.
+    + apply Nat.lt_le_incl.
+      apply fin_lt.
+  - apply Nat.Div0.mul_div_le.
+  - apply Nat.lt_le_pred.
+    apply mod2fin_lt.
+  - apply lt_sub_lt_add_l.
+    + apply Nat.lt_le_pred.
+      apply mod2fin_lt.
+    + apply Nat.lt_lt_add_l.
+      apply lt_pred_u.
+  - apply Nat.lt_le_pred.
+    apply fin_lt.
+  - apply Nat.lt_le_incl.
+    apply fin_lt.
 Qed.
 
 Lemma revf_addm : ∀ (f : fin u) (j : nat), revf (addm f j) = subm (revf f) j.
@@ -1117,12 +1130,22 @@ Proof using . intros. rewrite prefE, sucfE. apply symf_subf. Qed.
 Lemma addm_lt_large : ∀ (f : fin u) (j : nat),
   fin0 < f -> oppf f <= j mod u -> addm f j < f.
 Proof using .
-  intros * Hlt Hle. erewrite <- (Nat.mod_small f), <- Nat.mod_add, <- addm_mod,
+  intros * Hlt Hle. erewrite <- (Nat.mod_small f), <- Nat.Div0.mod_add, <- addm_mod,
   addm2nat, Nat.mul_1_l. eapply mod_lt_between_compat; try rewrite Nat.mul_1_r.
-  3: apply Nat.add_lt_mono_l. 1,2: split. 4: apply Nat.add_lt_mono_r.
-  3: apply Nat.le_add_l. 2: apply Nat.add_lt_mono. all: try apply fin_lt.
-  4: apply neq_u_0. 2,3: apply mod2fin_lt. eapply Nat.le_trans.
-  2: apply Nat.add_le_mono_l, Hle. rewrite addn_oppf. reflexivity. apply Hlt.
+  - split.
+    + eapply Nat.le_trans.
+      all:swap 1 2.
+      * apply Nat.add_le_mono_l, Hle.
+      * rewrite addn_oppf. reflexivity. apply Hlt.
+    + apply Nat.add_lt_mono;try apply fin_lt.
+      apply mod2fin_lt.
+  - split.
+    + apply Nat.le_add_l.
+    + apply Nat.add_lt_mono_r.
+      apply fin_lt.
+  - apply Nat.add_lt_mono_l.
+    apply mod2fin_lt.
+  - apply fin_lt.
 Qed.
 
 Lemma addm_le_small :
diff --git a/Util/NumberComplements.v b/Util/NumberComplements.v
index 76d8f79d365dd142169add4f488d903c77960a27..cd13e26dfad28438886b646a6245dd22f36f4c08 100644
--- a/Util/NumberComplements.v
+++ b/Util/NumberComplements.v
@@ -301,13 +301,13 @@ intros * Hne Hle Hsu Heq.
 rewrite (Nat.div_mod m p), (Nat.div_mod n p), Heq; trivial; [].
 apply Nat.add_cancel_r, Nat.mul_cancel_l; trivial; [].
 apply Nat.le_antisymm.
-+ apply Nat.div_le_mono. exact Hne. exact Hle.
++ apply Nat.Div0.div_le_mono. exact Hle.
 + apply Nat.sub_0_le, Nat.lt_1_r. rewrite (Nat.mul_lt_mono_pos_l p); try lia; [].
   rewrite Nat.mul_1_r, Nat.mul_sub_distr_l.
   assert (Hmod : ∀ x y : nat, y ≠ 0 -> x - x mod y = y * (x / y)).
-  { intros. rewrite Nat.mod_eq; trivial; [].
+  { intros. rewrite Nat.Div0.mod_eq; trivial; [].
     cut (y * (x / y) <= x); try lia; [].
-    rewrite (Nat.div_mod_eq x y) at 2. assert (HH := Nat.mod_le x y). lia. }
+    rewrite (Nat.div_mod_eq x y) at 2. assert (HH := Nat.Div0.mod_le x y). lia. }
   setoid_rewrite <- Hmod; lia.
 Qed.
 
@@ -356,17 +356,19 @@ Proof using . intros * []. symmetry. apply Nat.div_unique with (m - n * p); nia.
 Lemma mod_le_between_compat : ∀ p n m1 m2 : nat, n * p <= m1 < n * p + n
   -> n * p <= m2 < n * p + n -> m1 <= m2 -> m1 mod n <= m2 mod n.
 Proof using .
-  intros * H1 H2 Hle. erewrite 2 Nat.mod_eq, 2 between_muln,
-  Nat.add_le_mono_r, 2 Nat.sub_add. 6,7: eapply between_neq_0.
-  1,4-7: eassumption. apply H2. apply H1.
+  intros * H1 H2 Hle. erewrite 2 Nat.Div0.mod_eq, 2 between_muln,
+  Nat.add_le_mono_r, 2 Nat.sub_add;try assumption;try eassumption.
+  - apply H2.
+  - apply H1.
 Qed.
 
 Lemma mod_lt_between_compat : ∀ p n m1 m2 : nat, n * p <= m1 < n * p + n
   -> n * p <= m2 < n * p + n -> m1 < m2 -> m1 mod n < m2 mod n.
 Proof using .
-  intros * H1 H2 Hlt. erewrite 2 Nat.mod_eq, 2 between_muln,
-  Nat.add_lt_mono_r, 2 Nat.sub_add. 6,7: eapply between_neq_0.
-  1,4-7: eassumption. apply H2. apply H1.
+  intros * H1 H2 Hlt. erewrite 2 Nat.Div0.mod_eq, 2 between_muln,
+    Nat.add_lt_mono_r, 2 Nat.sub_add;try assumption; try eassumption.
+  - apply H2.
+  - apply H1.
 Qed.
 
 Lemma divide_neq : ∀ a b : nat, b ≠ 0 -> Nat.divide a b -> a ≠ 0.
@@ -375,9 +377,10 @@ Proof using . intros * Hn Hd H. subst. apply Hn, Nat.divide_0_l, Hd. Qed.
 Lemma divide_div_neq : ∀ a b : nat, b ≠ 0 -> Nat.divide a b -> b / a ≠ 0.
 Proof using .
   intros * Hn Hd H. apply Hn. unshelve erewrite (Nat.div_mod b a),
-  (proj2 (Nat.mod_divide b a _)), Nat.add_0_r, H. 2: apply Nat.mul_0_r.
-  1,3: eapply divide_neq. all: eassumption.
-Qed.
+  (proj2 (Nat.Lcm0.mod_divide b a)), Nat.add_0_r, H; try eassumption.
+  - apply Nat.mul_0_r.
+  - eapply divide_neq; eassumption.
+  Qed.
 
 Lemma addn_muln_divn : ∀ n q1 q2 r1 r2 : nat, n ≠ 0 -> r1 < n -> r2 < n
   -> n * q1 + r1 = n * q2 + r2 -> q1 = q2 ∧ r1 = r2.
@@ -390,16 +393,17 @@ Qed.
 Lemma divide_mul : ∀ a b : nat, b ≠ 0 -> Nat.divide a b -> b = a * (b / a).
 Proof using .
   intros * Hn Hd. erewrite (Nat.div_mod b a) at 1.
-  unshelve erewrite (proj2 (Nat.mod_divide b a _)). 2: apply Nat.add_0_r.
-  1,3: eapply divide_neq. all: eassumption.
+  unshelve erewrite (proj2 (Nat.Lcm0.mod_divide b a )); try eassumption.
+  - apply Nat.add_0_r.
+  - eapply divide_neq;eassumption.
 Qed.
 
 Lemma divide_mod :
   ∀ a b c : nat, b ≠ 0 -> Nat.divide a b -> (c mod b) mod a = c mod a.
 Proof using .
-  intros * Hn Hd. rewrite (divide_mul a b), Nat.mod_mul_r, Nat.mul_comm,
-  Nat.mod_add. apply Nat.mod_mod. 4: apply divide_div_neq.
-  1-3: eapply divide_neq. all: eassumption.
+  intros * Hn Hd. rewrite (divide_mul a b), Nat.Div0.mod_mul_r, Nat.mul_comm,
+  Nat.Div0.mod_add; try assumption.
+  apply Nat.Div0.mod_mod.
 Qed.
 
 Lemma mul_add : ∀ a b : nat,