From a373a0b238b052fc7f01c0ab02d68df6acb7c17e Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Date: Mon, 7 Oct 2024 17:45:45 +0200
Subject: [PATCH] Compiles with coq-8.19

---
 CaseStudies/Convergence/Impossibility_2G_1B.v |  1 -
 .../Exploration/ImpossibilityKDividesN.v      |  5 ++-
 CaseStudies/Gathering/Definitions.v           |  1 -
 CaseStudies/Gathering/Impossibility.v         |  4 +-
 CaseStudies/Gathering/InR/Algorithm.v         | 42 +++++++++----------
 CaseStudies/Gathering/InR/Impossibility.v     |  3 +-
 CaseStudies/Gathering/InR2/Algorithm.v        | 41 +++++++++---------
 .../Gathering/InR2/FSyncFlexNoMultAlgorithm.v |  3 +-
 CaseStudies/Gathering/InR2/Peleg.v            |  3 +-
 CaseStudies/Gathering/WithMultiplicity.v      |  2 +-
 CaseStudies/LifeLine/Algorithm.v              |  2 +-
 Models/GraphEquivalence.v                     |  4 +-
 Spaces/R.v                                    |  1 -
 Util/FMaps/FMapFacts.v                        |  9 ++--
 Util/ListComplements.v                        |  2 +-
 Util/MMultiset/Preliminary.v                  |  1 -
 Util/Preliminary.v                            |  1 +
 17 files changed, 63 insertions(+), 62 deletions(-)

diff --git a/CaseStudies/Convergence/Impossibility_2G_1B.v b/CaseStudies/Convergence/Impossibility_2G_1B.v
index a300bc19..42eb1044 100644
--- a/CaseStudies/Convergence/Impossibility_2G_1B.v
+++ b/CaseStudies/Convergence/Impossibility_2G_1B.v
@@ -22,7 +22,6 @@ 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.
diff --git a/CaseStudies/Exploration/ImpossibilityKDividesN.v b/CaseStudies/Exploration/ImpossibilityKDividesN.v
index fe6c098b..a428f6e0 100644
--- a/CaseStudies/Exploration/ImpossibilityKDividesN.v
+++ b/CaseStudies/Exploration/ImpossibilityKDividesN.v
@@ -211,7 +211,10 @@ Proof using Hmove kdn k_inf_n ltc_0_k.
     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.
-    intros [_ Habs]. contradiction (lt_not_le _ _ k_inf_n). rewrite local_subproof1,
+    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.
   * apply IHvisited. rewrite Heq_e, execute_tail. rewrite round_id. f_equiv.
diff --git a/CaseStudies/Gathering/Definitions.v b/CaseStudies/Gathering/Definitions.v
index ba3dd1de..c144450b 100644
--- a/CaseStudies/Gathering/Definitions.v
+++ b/CaseStudies/Gathering/Definitions.v
@@ -19,7 +19,6 @@
 (**************************************************************************)
 
 
-Require Import Arith.Div2.
 Require Import Lia.
 Require Export SetoidDec.
 Require Export Pactole.Util.Preliminary.
diff --git a/CaseStudies/Gathering/Impossibility.v b/CaseStudies/Gathering/Impossibility.v
index 0ce445e8..24d98e24 100644
--- a/CaseStudies/Gathering/Impossibility.v
+++ b/CaseStudies/Gathering/Impossibility.v
@@ -17,7 +17,7 @@
      This file is distributed under the terms of the CeCILL-C licence.    *)
 (**************************************************************************)
 
-Require Import Reals Psatz Morphisms Arith.Div2 Lia List SetoidList.
+Require Import Reals Psatz Morphisms Lia List SetoidList.
 From Pactole Require Import Util.Preliminary Util.Fin.
 Require Import Pactole.Setting.
 Require Import Pactole.Spaces.EuclideanSpace.
@@ -204,7 +204,7 @@ destruct (Nat.eq_dec (from_elements (List.map (fun x : location => (x, 1)) l))[e
          change (InA eq_pair (e, (from_elements (List.map (fun y => (y, 1)) l))[e])
                              (elements (from_elements (List.map (fun y => (y, 1)) l)))).
          rewrite elements_spec; simpl.
-         split; trivial; []. apply neq_0_lt. auto.
+         split; trivial; []. apply Nat.neq_0_lt_0. auto.
       -- revert_all.
          rewrite removeA_InA; autoclass. tauto.
 Qed.
diff --git a/CaseStudies/Gathering/InR/Algorithm.v b/CaseStudies/Gathering/InR/Algorithm.v
index 6b154dd9..7ce328a4 100644
--- a/CaseStudies/Gathering/InR/Algorithm.v
+++ b/CaseStudies/Gathering/InR/Algorithm.v
@@ -18,7 +18,6 @@
 (**************************************************************************)
 
 Require Import Bool.
-Require Import Arith.Div2.
 Require Import Lia.
 Require Import Rbase Rbasic_fun.
 Require Import List SetoidList.
@@ -181,7 +180,7 @@ intros config pt. split; intro Hmaj.
     split; intro Hpt.
     - rewrite Hpt. intro x. destruct (Rdec x pt).
       -- subst x. reflexivity.
-      -- apply lt_le_weak. now apply (Hmaj x).
+      -- apply Nat.lt_le_incl. now apply (Hmaj x).
     - destruct (Rdec y pt) as [? | Hy]; trivial.
       exfalso. apply (Hmaj y) in Hy. specialize (Hpt pt). simpl in *. lia.
 * intros x Hx. apply max_spec_lub.
@@ -216,7 +215,7 @@ rewrite <- (@cardinal_total_sub_eq _ _ _ _ _ (add pt2 (Nat.div2 nG) (singleton p
     - repeat destruct_match; simpl in *; contradiction || lia.
     - assumption.
 * rewrite cardinal_add, cardinal_singleton, cardinal_obs_from_config.
-  simpl. rewrite plus_0_r. now apply even_div2.
+  simpl. rewrite Nat.add_0_r. now apply even_div2.
 Qed.
 
 Lemma support_max_1_not_invalid : forall config pt,
@@ -244,7 +243,7 @@ assert (Hpt : pt = pt1 \/ pt = pt2).
   { rewrite <- Hsup, <- InA_Leibniz. change eq with (@equiv location _).
     rewrite support_spec, <- max_subset, <- support_spec, Hmaj. now left. }
   inversion_clear Hin; auto. inversion_clear H; auto. inversion H0. }
-apply (lt_irrefl (Nat.div2 nG)). destruct Hpt; subst pt.
+apply (Nat.lt_irrefl (Nat.div2 nG)). destruct Hpt; subst pt.
 - rewrite <- Hpt1 at 2. rewrite <- Hpt2. apply max_spec_lub; try (now rewrite Hmax).
 - rewrite <- Hpt1 at 1. rewrite <- Hpt2. apply max_spec_lub; now rewrite Hmax.
 Qed.
@@ -424,7 +423,7 @@ Lemma not_invalid_not_majority_length : forall config,
 Proof using size_G.
 intros config H1 H2.
 assert (size (!! config) > 1)%nat.
-{ unfold gt. eapply lt_le_trans; try eassumption.
+{ unfold gt. eapply Nat.lt_le_trans; try eassumption.
   f_equiv. apply max_subset. }
 destruct (size (!! config)) as [| [| [| ?]]] eqn:Hlen; try lia.
 exfalso. apply H2. now rewrite invalid_equiv.
@@ -596,7 +595,7 @@ Definition gatherR_pgm (s : observation) : location :=
     | nil => 0 (* only happen with no robots *)
     | pt :: nil => pt (* case 1: one majority stack *)
     | _ => (* several majority stacks *)
-           if beq_nat (size s) 3
+           if Nat.eqb (size s) 3
            then middle s else
            if is_extremal 0 s then 0 else extreme_center s
   end.
@@ -633,7 +632,7 @@ Lemma round_simplify : forall config,
                        | nil => config id (* only happen with no robots *)
                        | pt :: nil => pt (* case 1: one majority stack *)
                        | _ => (* several majority stacks *)
-                              if beq_nat (size s) 3
+                              if Nat.eqb (size s) 3
                               then middle s else
                               if is_extremal (config id) s then config id else extreme_center s
                      end
@@ -793,9 +792,10 @@ Theorem MajTower_at_forever : forall pt config,
   MajTower_at pt config -> MajTower_at pt (round gatherR da config).
 Proof using Hda size_G.
 intros pt config Hmaj x Hx. assert (Hs := Hmaj x Hx).
-apply le_lt_trans with ((!! config)[x]); try eapply lt_le_trans; try eassumption; [|].
+apply Nat.le_lt_trans with ((!! config)[x]).
 - eapply Majority_wither; eauto.
-- eapply Majority_grow; eauto.
+- apply Nat.lt_le_trans with (!! config)[pt]; try eassumption; [].
+  eapply Majority_grow; eauto.
 Qed.
 
 Theorem Majority_not_invalid : forall pt config, MajTower_at pt config -> ~WithMultiplicity.invalid config.
@@ -825,7 +825,7 @@ Lemma Generic_min_max_lt : forall config,
   no_Majority config -> mini (!! config) < maxi (!! config).
 Proof using size_G.
 intros config Hmaj. apply Generic_min_max_lt_aux.
-+ apply lt_le_trans with (size (max (!! config))); trivial.
++ apply Nat.lt_le_trans with (size (max (!! config))); trivial.
   rewrite <- size_spec. f_equiv. apply max_subset.
 + apply support_NoDupA.
 Qed.
@@ -1084,7 +1084,7 @@ Proof using .
     assert (Hg : forall id, get_location (round r da config id) <> pt \/ get_location (config id) = pt).
     { intro id. specialize (Hex id (In_names _)). revert Hex. repeat destruct_match; auto. }
     (** We prove a contradiction by showing that the opposite inequality of Hlt holds. *)
-    clear Hex. revert Hlt. apply le_not_lt.
+    clear Hex. revert Hlt. apply Nat.le_ngt.
     do 2 rewrite obs_from_config_spec, config_list_spec.
     induction names as [| id l]; simpl; trivial; [].
     unfold Datatypes.id in *. repeat destruct_match; auto using le_n_S; [].
@@ -1183,7 +1183,7 @@ destruct (support (max (!! config))) as [| pt [| pt' l']] eqn:Hmaj.
     { intros id Hid.
       rewrite <- Hrmove_pt.
       apply same_destination; auto. rewrite moving_spec. congruence. }
-    assert ((div2 nG) <= (!! config)[pt']).
+    assert ((Nat.div2 nG) <= (!! config)[pt']).
     { transitivity ((!! (round gatherR da config))[pt']).
       - decompose [and or] Hpt; subst.
         + setoid_rewrite  Hpt2. reflexivity.
@@ -1195,18 +1195,18 @@ destruct (support (max (!! config))) as [| pt [| pt' l']] eqn:Hmaj.
         rewrite <- Hid1.
         symmetry.
         apply Hdest. rewrite moving_spec. assumption. }
-    assert (Hlt : forall p, p <> pt' -> (!! config)[p] < div2 nG).
+    assert (Hlt : forall p, p <> pt' -> (!! config)[p] < Nat.div2 nG).
     { assert (Hpt'_in : In pt' (!! config)).
-      { unfold In. eapply lt_le_trans; try eassumption. apply half_size_config. }
+      { unfold In. eapply Nat.lt_le_trans; try eassumption. apply half_size_config. }
       assert (Hle := not_invalid_not_majority_length Hmaj Hok).
-      intros p Hp. apply Nat.nle_gt. intro Habs. apply (lt_irrefl nG).
+      intros p Hp. apply Nat.nle_gt. intro Habs. apply (Nat.lt_irrefl nG).
       destruct (@towers_elements_3 config pt' p Hle Hpt'_in) as [pt3' [Hdiff13 [Hdiff23 Hpt3_in]]]; trivial.
-      + apply lt_le_trans with (div2 nG); try assumption. apply half_size_config.
+      + apply Nat.lt_le_trans with (Nat.div2 nG); try assumption. apply half_size_config.
       + auto.
-      + eapply lt_le_trans; try apply (sum3_le_total config Hp Hdiff13 Hdiff23); [].
+      + eapply Nat.lt_le_trans; try apply (sum3_le_total config Hp Hdiff13 Hdiff23); [].
         unfold In in Hpt3_in. rewrite <- (even_div2 _ HnG). lia. }
     assert (Hmaj' : MajTower_at pt' config).
-    { intros x Hx. apply lt_le_trans with (div2 nG); trivial. now apply Hlt. }
+    { intros x Hx. apply Nat.lt_le_trans with (Nat.div2 nG); trivial. now apply Hlt. }
     apply MajTower_at_forever, Majority_not_invalid in Hmaj'. contradiction. }
 Qed.
 
@@ -1219,7 +1219,7 @@ Definition config_to_NxN config :=
     | nil => (0, 0)
     | pt :: nil => (1, nG - s[pt])
     | _ :: _ :: _ =>
-        if beq_nat (size s) 3
+        if Nat.eqb (size s) 3
         then (2, nG - s[nth 1 (sort (support s)) 0%R])
         else (3, nG - (s[extreme_center s]
                        + s[hd 0%R (sort  (support s))]
@@ -1364,7 +1364,7 @@ destruct (support (max (!! config))) as [| pt [| ? ?]] eqn:Hmaj.
       assert (Hmaj' : no_Majority (round gatherR da config)).
       { unfold no_Majority. rewrite size_spec, Hmaj''. simpl. lia. } clear Hmaj''.
       assert (Hlen' : size (!! (round gatherR da config)) = 3).
-      { apply le_antisym.
+      { apply Nat.le_antisymm.
         + apply (support_decrease Hmaj Hlen).
         + apply (not_invalid_not_majority_length Hmaj'). now apply never_invalid. }
       rewrite (config_to_NxN_Three_spec Hmaj' Hlen'). apply Lexprod.right_lex.
@@ -1464,7 +1464,7 @@ Lemma not_invalid_gathered_Majority_size : forall config id,
 Proof using size_G.
 intros config id Hinvalid Hgather Hmaj.
 assert (size (!! config) > 1).
-{ unfold no_Majority in Hmaj. eapply lt_le_trans; try eassumption; []. now rewrite max_subset. }
+{ unfold no_Majority in Hmaj. eapply Nat.lt_le_trans; try eassumption; []. now rewrite max_subset. }
 rewrite invalid_equiv in Hinvalid.
 destruct (size (!! config)) as [| [| [| ?]]]; lia || tauto.
 Qed.
diff --git a/CaseStudies/Gathering/InR/Impossibility.v b/CaseStudies/Gathering/InR/Impossibility.v
index baec2093..6574320e 100644
--- a/CaseStudies/Gathering/InR/Impossibility.v
+++ b/CaseStudies/Gathering/InR/Impossibility.v
@@ -20,7 +20,6 @@
 Require Import Reals.
 Require Import Psatz.
 Require Import Morphisms.
-Require Import Arith.Div2.
 Require Import Lia.
 Require Import List SetoidList.
 Require Import Pactole.Util.Preliminary Pactole.Util.Fin.
@@ -169,7 +168,7 @@ destruct (Nat.eq_dec (from_elements (List.map (fun x : location => (x, 1)) l))[e
          change (InA eq_pair (e, (from_elements (List.map (fun x0 : R => (x0, 1)) l))[e])
                              (elements (from_elements (List.map (fun x : location => (x, 1)) l)))).
          rewrite elements_spec; simpl.
-         split; trivial; []. apply neq_0_lt. auto.
+         split; trivial; []. apply Nat.neq_0_lt_0. auto.
       -- revert_all.
          rewrite removeA_InA; autoclass. tauto.
 Qed.
diff --git a/CaseStudies/Gathering/InR2/Algorithm.v b/CaseStudies/Gathering/InR2/Algorithm.v
index 1cf963fc..f17aa035 100644
--- a/CaseStudies/Gathering/InR2/Algorithm.v
+++ b/CaseStudies/Gathering/InR2/Algorithm.v
@@ -19,7 +19,6 @@
 
 
 Require Import Bool.
-Require Import Arith.Div2.
 Require Import Lia Field Lra.
 Require Import Rbase Rbasic_fun R_sqrt Rtrigo_def.
 Require Import List.
@@ -127,7 +126,7 @@ Ltac changeR2 :=
 Lemma config_list_alls : forall pt, config_list (fun _ => pt) = alls pt nG.
 Proof using .
 intro. rewrite config_list_spec, map_cst.
-rewrite names_length. simpl. now rewrite plus_0_r.
+rewrite names_length. simpl. now rewrite Nat.add_0_r.
 Qed.
 
 Lemma no_byz_eq : forall config1 config2 : configuration,
@@ -360,10 +359,10 @@ intros config pt. split; intro Hmaj.
     simpl equiv. split; intro Hpt.
     - subst y. intro x. destruct (equiv_dec x pt).
       -- rewrite e. reflexivity.
-      -- apply lt_le_weak. now apply (Hmaj x).
+      -- apply Nat.lt_le_incl. now apply (Hmaj x).
     - destruct (equiv_dec y pt) as [? | Hy]; trivial.
-      exfalso. apply (Hmaj y) in Hy. contradiction (lt_irrefl (!! config)[pt]).
-      eapply le_lt_trans; try eassumption; [].
+      exfalso. apply (Hmaj y) in Hy. contradiction (Nat.lt_irrefl (!! config)[pt]).
+      eapply Nat.le_lt_trans; try eassumption; [].
       apply Hpt.
 * intros x Hx. apply max_spec_lub.
   - rewrite <- support_spec, Hmaj. now left.
@@ -471,7 +470,7 @@ assert (Hpt : pt = pt1 \/ pt = pt2).
     setoid_rewrite Hmaj.
     now left. }
 inversion_clear Hin; auto. inversion_clear H0; auto. inversion H1. }
-apply (lt_irrefl (Nat.div2 nG)). destruct Hpt; subst pt.
+apply (Nat.lt_irrefl (Nat.div2 nG)). destruct Hpt; subst pt.
 - rewrite <- Hpt1 at 2. rewrite <- Hpt2. apply max_spec_lub; try now rewrite Hmax.
 - rewrite <- Hpt1 at 1. rewrite <- Hpt2. apply max_spec_lub; now rewrite Hmax.
 Qed.
@@ -644,7 +643,7 @@ Lemma not_invalid_no_majority_size : forall config,
 Proof using size_G.
 intros config H1 H2.
 assert (size (!! config) > 1)%nat.
-{ unfold gt. eapply lt_le_trans; try eassumption; []. f_equiv. apply max_subset. }
+{ unfold gt. eapply Nat.lt_le_trans; try eassumption; []. f_equiv. apply max_subset. }
  destruct (size (!! config)) as [| [| [| ?]]] eqn:Hlen; try lia.
 exfalso. apply H2. now rewrite invalid_equiv.
 Qed.
@@ -683,7 +682,7 @@ Qed.
 Lemma SECT_cardinal_le_nG : forall config, SECT_cardinal (!! config) <= nG.
 Proof using .
 intro config. unfold SECT_cardinal.
-replace nG with (nG + nB) by (simpl; apply plus_0_r).
+replace nG with (nG + nB) by (simpl; apply Nat.add_0_r).
 rewrite <- (cardinal_obs_from_config config origin).
 apply cardinal_sub_compat, filter_subset.
 intros ? ? H. now rewrite H.
@@ -1246,7 +1245,7 @@ destruct (existsb (fun x => if get_location (round r da config x) =?= pt then
   assert (Hg : forall id, get_location (round r da config id) <> pt \/ get_location (config id) = pt).
   { intro id. specialize (Hex id (In_names _)). revert Hex. repeat destruct_match; try discriminate; auto. }
   (** We prove a contradiction by showing that the opposite inequality of Hlt holds. *)
-  clear Hex. revert Hlt. apply le_not_lt.
+  clear Hex. revert Hlt. apply Nat.le_ngt.
   setoid_rewrite WithMultiplicity.obs_from_config_spec.
   do 2 rewrite config_list_spec.
   induction names as [| id l]; trivial; [].
@@ -1483,7 +1482,7 @@ Theorem MajTower_at_forever : forall pt config,
   MajTower_at pt config -> MajTower_at pt (round gatherR2 da config).
 Proof using Hssync.
 intros pt config Hmaj x Hx. assert (Hs := Hmaj x Hx).
-apply le_lt_trans with ((!! config)[x]); try eapply lt_le_trans; try eassumption; [|].
+apply Nat.le_lt_trans with ((!! config)[x]); try eapply Nat.lt_le_trans; try eassumption; [|].
 - eapply Majority_wither; eauto.
 - eapply Majority_grow; eauto.
 Qed.
@@ -1692,7 +1691,7 @@ destruct (support (max (!! config))) as [| pt [| pt' l']] eqn:Hmaj.
     assert (Hdest : forall g, List.In g (moving gatherR2 da config) ->
                     get_location (round gatherR2 da config g) == pt).
     { intros id Hid. rewrite <- Hrmove_pt. apply same_destination; auto. rewrite moving_spec. congruence. }
-    assert ((div2 nG) <= (!! config)[pt']).
+    assert ((Nat.div2 nG) <= (!! config)[pt']).
     { transitivity ((!! (round gatherR2 da config))[pt']).
       - decompose [and or] Hpt; clear Hpt; subst.
         + setoid_rewrite Hpt2. simpl. reflexivity.
@@ -1704,19 +1703,21 @@ destruct (support (max (!! config))) as [| pt [| pt' l']] eqn:Hmaj.
         rewrite <- Hid1.
         symmetry.
         apply Hdest. rewrite moving_spec. intro Habs. apply Hid2. now rewrite Habs. }
-    assert (Hlt : forall p, p <> pt' -> (!! config)[p] < div2 nG).
+    assert (Hlt : forall p, p <> pt' -> (!! config)[p] < Nat.div2 nG).
     { assert (Hpt'_in : In pt' (!! config)).
-      { unfold In. eapply lt_le_trans; try eassumption. apply Exp_prop.div2_not_R0. apply HsizeG. }
+      { unfold In. eapply Nat.lt_le_trans; try eassumption. apply Exp_prop.div2_not_R0. apply HsizeG. }
       assert (Hle := not_invalid_no_majority_size Hmaj Hok).
-      intros p Hp. apply Nat.nle_gt. intro Habs. apply (lt_irrefl nG).
+      intros p Hp. apply Nat.nle_gt. intro Habs. apply (Nat.lt_irrefl nG).
       destruct (@towers_elements_3 config pt' p Hle Hpt'_in) as [pt3' [Hdiff13 [Hdiff23 Hpt3_in]]]; trivial.
-      + apply lt_le_trans with (div2 nG); try assumption. apply Exp_prop.div2_not_R0. apply HsizeG.
+      + apply Nat.lt_le_trans with (Nat.div2 nG); try assumption. apply Exp_prop.div2_not_R0. apply HsizeG.
       + auto.
-      + eapply lt_le_trans; try apply (sum3_le_total config Hp Hdiff13 Hdiff23); [].
-        unfold In in Hpt3_in. rewrite <- ?Even.even_equiv in *.
-        rewrite (even_double nG); auto. unfold Nat.double. lia. }
+      + eapply Nat.lt_le_trans; try apply (sum3_le_total config Hp Hdiff13 Hdiff23); [].
+        unfold In in Hpt3_in. rewrite <- ?Nat.Even_alt_Even in *.
+        rewrite (Nat.Even_double nG).
+        2:{ now apply Nat.Even_alt_Even. }
+        unfold Nat.double. lia. }
     assert (Hmaj' : MajTower_at pt' config).
-    { intros x Hx. apply lt_le_trans with (div2 nG); trivial. now apply Hlt. }
+    { intros x Hx. apply Nat.lt_le_trans with (Nat.div2 nG); trivial. now apply Hlt. }
     apply MajTower_at_equiv in Hmaj'.
     red in Hmaj.
     rewrite size_spec in Hmaj.
@@ -2631,7 +2632,7 @@ destruct (support (max (!! (round gatherR2 da config)))) as [| pt1 [| pt2 l]] eq
          ++ assert (Hperm' : PermutationA equiv (support (!! (round gatherR2 da config)))
                                                 (isobarycenter_3_pts ptx pty ptz :: ptx :: pty :: ptz :: nil)).
             { assert ((!! (round gatherR2 da config))[target (!! config)] > 0).
-              { apply le_lt_trans with ((!! config)[target (!! config)]); try lia.
+              { apply Nat.le_lt_trans with ((!! config)[target (!! config)]); try lia.
                 rewrite increase_move_iff.
                 exists gmove. split.
                 - apply destination_is_target; trivial.
diff --git a/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v b/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
index e931c98c..ece8453a 100644
--- a/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
+++ b/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
@@ -10,7 +10,6 @@
 (**************************************************************************)
 
 Require Import Bool.
-Require Import Arith.Div2.
 Require Import Lia Field.
 Require Import Rbase Rbasic_fun R_sqrt Rtrigo_def.
 Require Import List.
@@ -127,7 +126,7 @@ Proof using . intros ? ? Heq. apply no_byz_eq. intro. apply Heq. Qed.
 Lemma config_list_alls : forall pt, config_list (fun _ => pt) = alls pt nG.
 Proof using .
 intro. rewrite config_list_spec, map_cst.
-rewrite names_length. simpl. now rewrite plus_0_r.
+rewrite names_length. simpl. now rewrite Nat.add_0_r.
 Qed.
 
 (** Define one robot to get their location whenever they are gathered. *)
diff --git a/CaseStudies/Gathering/InR2/Peleg.v b/CaseStudies/Gathering/InR2/Peleg.v
index 8883e621..18c9b78d 100644
--- a/CaseStudies/Gathering/InR2/Peleg.v
+++ b/CaseStudies/Gathering/InR2/Peleg.v
@@ -10,7 +10,6 @@
 (**************************************************************************)
 
 Require Import Bool.
-Require Import Arith.Div2.
 Require Import Lia Field.
 Require Import Rbase Rbasic_fun R_sqrt Rtrigo_def.
 Require Import List.
@@ -126,7 +125,7 @@ Lemma config_list_alls : forall pt, config_list (fun _ => pt) = alls pt nG.
 Proof using .
 intro. rewrite config_list_spec, map_cst.
 Typeclasses eauto := (bfs) 10.
-setoid_rewrite names_length. simpl. now rewrite plus_0_r.
+setoid_rewrite names_length. simpl. now rewrite Nat.add_0_r.
 Qed.
 Typeclasses eauto := (dfs).
 
diff --git a/CaseStudies/Gathering/WithMultiplicity.v b/CaseStudies/Gathering/WithMultiplicity.v
index 4bf58d6f..65285e01 100644
--- a/CaseStudies/Gathering/WithMultiplicity.v
+++ b/CaseStudies/Gathering/WithMultiplicity.v
@@ -27,7 +27,7 @@ Close Scope R_scope.
 Close Scope VectorSpace_scope.
 Set Implicit Arguments.
 Typeclasses eauto := (bfs) 5.
-Require Even.
+(* Require Even. *)
 
 (** Gathering Definitions specific to a setting with multiplicities, i.e. a multiset observation. *)
 
diff --git a/CaseStudies/LifeLine/Algorithm.v b/CaseStudies/LifeLine/Algorithm.v
index f7f9121d..633f29ac 100644
--- a/CaseStudies/LifeLine/Algorithm.v
+++ b/CaseStudies/LifeLine/Algorithm.v
@@ -1,6 +1,6 @@
 Require Import Utf8.
 Require Import Bool.
-Require Import Arith.Div2 Lia Field.
+Require Import Lia Field.
 Require Import Rbase Rbasic_fun R_sqrt Rtrigo_def Lra.
 Require Import List SetoidList SetoidDec.
 Require Import Relations RelationPairs Morphisms.
diff --git a/Models/GraphEquivalence.v b/Models/GraphEquivalence.v
index c13c77fe..8ea39ff4 100644
--- a/Models/GraphEquivalence.v
+++ b/Models/GraphEquivalence.v
@@ -676,7 +676,9 @@ simpl activate. destruct_match_eq Hactive.
                                == iso_E (inverse Ciso) e).
     { destruct (precondition_satisfied_inv da config g)as [Ciso' [HCf HCt]].
       simpl projT1. intro e.
-      cut (bijectionG Ciso' (OnEdge e (1 /sr 2)) == bijectionG (inverse Ciso) (OnEdge e (1 /sr 2)));
+      (* why does this stopped working between coq-8.16 and 8.19? *)
+      (* cut ((bijectionG Ciso' (OnEdge e (1 /sr 2))) == (bijectionG (inverse Ciso) (OnEdge e (1 /sr 2)))). *)
+      cut (@equiv loc _ (bijectionG Ciso' (OnEdge e (1 /sr 2))) (bijectionG (inverse Ciso) (OnEdge e (1 /sr 2))));
       try (now intros [Heq _]); [].
       rewrite <- (HCf (OnEdge e (1 /sr 2))). reflexivity. }
     assert (HnotOnEdge : forall e p, Clocal_config (Good g) =/= SOnEdge e p).
diff --git a/Spaces/R.v b/Spaces/R.v
index 3a889734..dda1209f 100644
--- a/Spaces/R.v
+++ b/Spaces/R.v
@@ -20,7 +20,6 @@
 
 
 Require Import Bool.
-Require Import Arith.Div2.
 Require Import Lia.
 Require Export Rbase Rbasic_fun.
 Require Import Sorting.
diff --git a/Util/FMaps/FMapFacts.v b/Util/FMaps/FMapFacts.v
index 4bc52772..8f84f877 100644
--- a/Util/FMaps/FMapFacts.v
+++ b/Util/FMaps/FMapFacts.v
@@ -28,7 +28,7 @@ Section WeakFacts.
 
   Lemma eq_bool_alt : forall b b', b=b' <-> (b=true <-> b'=true).
   Proof using .
-    destruct b; destruct b'; intuition.
+    destruct b; destruct b'; clear; intuition.
   Qed.
 
   Lemma eq_option_alt : forall (elt:Type)(o o':option elt),
@@ -714,9 +714,10 @@ Section WeakFacts.
 
   Global Instance Empty_m elt : Proper (Equal ==> iff) (@Empty key _ _ _ elt).
   Proof using HF.
-    unfold Empty; intros m m' Hm; intuition.
-    rewrite <-Hm in H0; eauto.
-    rewrite Hm in H0; eauto.
+    unfold Empty; intros m m' Hm.
+    split; repeat intro.
+    - rewrite <-Hm in H0; eapply H;eauto.
+    - rewrite Hm in H0; eapply H;eauto.
   Qed.
 
   Global Instance is_empty_m elt :
diff --git a/Util/ListComplements.v b/Util/ListComplements.v
index c56c052a..e9313e9e 100644
--- a/Util/ListComplements.v
+++ b/Util/ListComplements.v
@@ -24,7 +24,7 @@ Require Import List SetoidList.
 Require Export SetoidPermutation.
 Require Import Sorting.Permutation.
 Require Import Bool.
-Require Import Arith.Div2 Lia PeanoNat.
+Require Import Lia PeanoNat.
 Require Import Psatz.
 Require Import SetoidDec.
 Require Import Pactole.Util.Preliminary.
diff --git a/Util/MMultiset/Preliminary.v b/Util/MMultiset/Preliminary.v
index d61eabfe..8713599e 100644
--- a/Util/MMultiset/Preliminary.v
+++ b/Util/MMultiset/Preliminary.v
@@ -10,7 +10,6 @@
 
 
 Require Import Lia.
-Require Import Arith.Div2.
 Require Import Reals.
 Require Import List.
 Require Import Morphisms.
diff --git a/Util/Preliminary.v b/Util/Preliminary.v
index 58551d1e..29c0edb2 100644
--- a/Util/Preliminary.v
+++ b/Util/Preliminary.v
@@ -20,6 +20,7 @@
 
 
 Require Import Utf8 Relations Morphisms SetoidClass.
+Require Logic.Decidable.
 Set Implicit Arguments.
 
 Ltac autoclass := eauto with typeclass_instances.
-- 
GitLab