diff --git a/CaseStudies/Convergence/Algorithm_noB.v b/CaseStudies/Convergence/Algorithm_noB.v
index c11fa60858a3a04b479b6148d14ee8bfa3b42352..48c4ed1bce14c65c481e954e9cf24f8ed308c233 100644
--- a/CaseStudies/Convergence/Algorithm_noB.v
+++ b/CaseStudies/Convergence/Algorithm_noB.v
@@ -24,6 +24,7 @@ Require Import SetoidDec.
 Require Import Lia.
 Require Import SetoidList.
 Require Import Pactole.Util.Preliminary.
+Require Import Pactole.Util.Bijection.
 Require Import Pactole.Util.Fin.
 Require Import Pactole.Setting.
 Require Import Pactole.Spaces.R2.
diff --git a/CaseStudies/Convergence/Impossibility_2G_1B.v b/CaseStudies/Convergence/Impossibility_2G_1B.v
index 648748d9d4420ae7bc4c21bc7071fb69cc91cb34..1c57cf28dfba680daff179ea0f204534b07a26c0 100644
--- a/CaseStudies/Convergence/Impossibility_2G_1B.v
+++ b/CaseStudies/Convergence/Impossibility_2G_1B.v
@@ -25,6 +25,7 @@ Require Import SetoidDec.
 Require Import Lia.
 Require Import SetoidList.
 Require Import Pactole.Util.Preliminary.
+Require Import Pactole.Util.Bijection.
 Require Import Pactole.Util.Fin.
 Require Import Pactole.Util.Enum.
 Require Import Pactole.Setting.
@@ -132,7 +133,7 @@ Proof using n_non_0.
 assert (Hn0 := n_non_0). rewrite nG_nB, nB_value.
 destruct n as [| ?].
 - lia.
-- cbn. rewrite Nat.add_comm. cbn. lia.
+- cbn. rewrite Nat.add_comm. cbn. auto with arith.
 Qed.
 
 (* TODO: move to a definition/problem file *)
@@ -186,7 +187,6 @@ Lemma synchro : ∀ r, solution r → solution_FSYNC r.
 Proof using . unfold solution. intros r Hfair config d Hd. apply Hfair, FSYNC_implies_Fair; autoclass. Qed.
 
 Close Scope R_scope.
-Close Scope vector_scope.
 
 
 (** We split good robots into two halves. *)
@@ -255,7 +255,6 @@ Hint Resolve gfirst_left glast_right left_right_exclusive : core.
     - the stack with byzantine is activated, good robots cannot move. *)
 
 Open Scope R_scope.
-Open Scope vector_scope.
 
 (** The reference starting configuration **)
 Definition config1 : configuration := fun id =>
@@ -379,8 +378,7 @@ intro pt. unfold observation1, observation2, swap. rewrite map_add, map_singleto
 cbn -[add singleton].
 ring_simplify (1 + -1 * (0 + -(1)) + -(1)).
 ring_simplify (1 + -1 * (1 + -(1)) + -(1)).
-destruct (Rdec pt 0); [| destruct (Rdec pt 1)]; subst;
-repeat rewrite ?add_same, ?singleton_same, ?singleton_other, ?add_other; auto.
+now rewrite <- add_singleton_comm.
 Qed.
 
 (** An execution alternating config1 and config2 *)
diff --git a/CaseStudies/Gathering/Impossibility.v b/CaseStudies/Gathering/Impossibility.v
index 2c23a8d18d20d9166e4fcf73de7527ec6aadbd71..ac16573c37feb01dc71961afa10365f782bd526d 100644
--- a/CaseStudies/Gathering/Impossibility.v
+++ b/CaseStudies/Gathering/Impossibility.v
@@ -19,10 +19,11 @@
 
 Require Import Reals Psatz Morphisms Lia List SetoidList.
 From Pactole Require Import Util.Preliminary Util.Fin.
+Require Import Pactole.Util.Bijection.
 Require Import Pactole.Setting.
 Require Import Pactole.Spaces.EuclideanSpace.
 Require Import Pactole.CaseStudies.Gathering.Definitions.
-Require Pactole.CaseStudies.Gathering.WithMultiplicity.
+Require Import Pactole.CaseStudies.Gathering.WithMultiplicity.
 Import Pactole.Observations.MultisetObservation.
 Require Import Pactole.Models.Rigid.
 Require Import Pactole.Models.NoByzantine.
@@ -52,7 +53,7 @@ Hypothesis nG_non_0 : n <> 0.
 Local Transparent G B.
 
 (** The setting is an arbitrary metric space over R. *)
-Context `{Location}.
+Context `{Loc:Location}.
 (* Instance St : State location := OnlyLocation (fun _ => True). *)
 Context {VS : RealVectorSpace location}.
 Context {ES : EuclideanSpace location}.
@@ -117,7 +118,7 @@ assert (Heven := even_nG). assert (HnG0 := nG_non_0).
 simpl. destruct n as [| [| ?]].
 - lia.
 - destruct Heven. lia.
-- simpl. lia.
+- simpl. solve [ auto with arith | lia].
 Qed.
 
 (* We need to unfold [obs_is_ok] for rewriting *)
diff --git a/CaseStudies/Gathering/InR/Algorithm.v b/CaseStudies/Gathering/InR/Algorithm.v
index 7b665695962ea2b4e207ebf2d3b895ebd396f7aa..09fe0415aace3c749d129f095d960111fca270b2 100644
--- a/CaseStudies/Gathering/InR/Algorithm.v
+++ b/CaseStudies/Gathering/InR/Algorithm.v
@@ -25,17 +25,17 @@ Require Import RelationPairs.
 Require Import Morphisms.
 Require Import Psatz.
 Require Import Inverse_Image.
-(* Pactole basic definitions *)
-Require Export Pactole.Setting.
 Require Import FMapFacts.
 (* Specific to R topology *)
 Require Import Pactole.Spaces.R.
 (* Specific to gathering *)
-Require Pactole.CaseStudies.Gathering.WithMultiplicity.
-(* I don't like this Import, but gathered_at is too frequent *)
-Require Import Pactole.CaseStudies.Gathering.Definitions.
+Require Import Pactole.CaseStudies.Gathering.WithMultiplicity.
+Require Import Pactole.Core.State.
 (* Specific to multiplicity *)
 Require Import Pactole.Observations.MultisetObservation.
+Require Import Pactole.Util.NumberComplements.
+(* I don't like this Import, but gathered_at is too frequent *)
+Require Import Pactole.CaseStudies.Gathering.Definitions.
 Require Import Pactole.Models.Similarity.
 (* Specific to rigidity *)
 Require Export Pactole.Models.Rigid.
@@ -48,7 +48,6 @@ Import Datatypes.
 Close Scope R_scope.
 
 (* rule of thumb *)
-Typeclasses eauto := 10.
 Set Implicit Arguments.
 
 (* this will become non default soon. *)
@@ -91,6 +90,8 @@ Instance InaFun : inactive_function unit := {
 Instance Rigid : RigidSetting.
 Proof using . split. reflexivity. Qed.
 
+Existing Instance multiset_observation.
+
 (* Trying to avoid notation problem with implicit arguments *)
 Notation "s [ x ]" := (multiplicity x s) (at level 2, no associativity, format "s [ x ]").
 Notation obs_from_config := (@obs_from_config _ _ _ _ multiset_observation).
@@ -104,7 +105,8 @@ Arguments origin : simpl never.
 Ltac changeR :=
   change R with location in *;
   change R_Setoid with location_Setoid in *;
-  change R_EqDec with location_EqDec in *.
+  change R_EqDec with location_EqDec in *;
+  change SetoidDefs.R_EqDec with (@location_EqDec Loc) in *.
 
 Lemma similarity_middle : forall (sim : similarity R) x y, (sim ((x + y) / 2) = (sim x + sim y) / 2)%R.
 Proof using .
@@ -130,7 +132,7 @@ apply Permutation_nil. setoid_rewrite Permuted_sort at 2. rewrite Habs. reflexiv
 Qed.
 
 Lemma half_size_config : Nat.div2 nG > 0.
-Proof using size_G. assert (Heven := size_G). simpl. destruct n as [| [| ?]]; simpl; lia. Qed.
+Proof using size_G. assert (Heven := size_G). simpl. destruct n as [| [| ?]]; simpl; solve [ auto with arith | lia]. Qed.
 
 (* We need to unfold [obs_is_ok] for rewriting *)
 Definition obs_from_config_spec : forall config l,
@@ -181,7 +183,7 @@ intros config pt. split; intro Hmaj.
   + intro y. rewrite InA_singleton.
     rewrite support_spec, max_spec1_iff; try (now apply obs_non_nil); [].
     split; intro Hpt.
-    - rewrite Hpt. intro x. destruct (Rdec x pt).
+    - rewrite Hpt. intro x. destruct (Req_dec_T x pt).
       -- subst x. reflexivity.
       -- apply Nat.lt_le_incl. now apply (Hmaj x).
     - destruct (Rdec y pt) as [? | Hy]; trivial.
@@ -193,26 +195,26 @@ Qed.
 
 (** **  Some properties of [invalid]  **)
 
-Lemma invalid_even : forall conf, WithMultiplicity.invalid conf -> Nat.Even nG.
+Lemma invalid_even : forall conf, (@WithMultiplicity.invalid Loc _ _ conf) -> Nat.Even nG.
 Proof using . now intros conf [? _]. Qed.
 
 Lemma invalid_support_length : forall config, WithMultiplicity.invalid config ->
   size (!! config) = 2.
 Proof using size_G.
 intros config [Heven [_ [pt1 [pt2 [Hdiff [Hpt1 Hpt2]]]]]].
-rewrite <- (@cardinal_total_sub_eq _ _ _ _ _ (add pt2 (Nat.div2 nG) (singleton pt1 (Nat.div2 nG)))).
+rewrite <- (@cardinal_total_sub_eq _ _ _ _ _ (MMultisetInterface.add pt2 (Nat.div2 nG) (singleton pt1 (Nat.div2 nG)))).
 * rewrite size_add; try (now apply half_size_config); [].
   destruct (In_dec pt2 (singleton pt1 (Nat.div2 nG))) as [Hin | Hin].
   + exfalso. rewrite In_singleton in Hin.
     destruct Hin. now contradiction Hdiff.
   + rewrite size_singleton; trivial. apply half_size_config.
-* intro pt. destruct (Rdec pt pt2), (Rdec pt pt1); subst.
+* intro pt. destruct (Req_dec_T pt pt2), (Req_dec_T pt pt1); subst.
   + now contradiction Hdiff.
   + rewrite add_spec, singleton_spec.
     setoid_rewrite Hpt2.
     repeat destruct_match; simpl in *; contradiction || (try lia).
   + rewrite add_other, singleton_spec.
-    - setoid_rewrite Hpt1. repeat destruct_match; simpl in *; contradiction || lia.
+    - changeR. setoid_rewrite Hpt1. repeat destruct_match; simpl in *; contradiction || lia.
     - assumption.
   + rewrite add_other, singleton_spec.
     - repeat destruct_match; simpl in *; contradiction || lia.
@@ -244,6 +246,7 @@ assert (Hsup : Permutation (support (!! config)) (pt1 :: pt2 :: nil)).
 assert (Hpt : pt = pt1 \/ pt = pt2).
 { assert (Hin : List.In pt (pt1 :: pt2 :: nil)).
   { rewrite <- Hsup, <- InA_Leibniz. change eq with (@equiv location _).
+    changeR.
     rewrite support_spec, <- max_subset, <- support_spec, Hmaj. now left. }
   inversion_clear Hin; auto. inversion_clear H; auto. inversion H0. }
 apply (Nat.lt_irrefl (Nat.div2 nG)). destruct Hpt; subst pt.
@@ -320,8 +323,8 @@ Proof using size_G.
         constructor 1.
         reflexivity. }
       assert (heq_config: equiv (!!config)
-                                (add pt1 ((!! config)[pt1])
-                                          (add pt2 ((!! config)[pt2]) empty))).
+                                (MMultisetInterface.add pt1 ((!! config)[pt1])
+                                          (MMultisetInterface.add pt2 ((!! config)[pt2]) empty))).
       { intros x.
         destruct (equiv_dec x pt1) as [heqxpt1 | hneqxpt1].
         - rewrite heqxpt1.
@@ -356,7 +359,7 @@ Proof using size_G.
         - intros ? ? ? ? ? Heq; subst; now rewrite Heq.
         - intros. lia.
         - symmetry.
-          transitivity ((pt1, (!! config)[pt1]) :: (elements (add pt2 (!! config)[pt2] empty))).
+          transitivity ((pt1, (!! config)[pt1]) :: (elements (MMultisetInterface.add pt2 (!! config)[pt2] empty))).
           eapply elements_add_out;auto.
           + rewrite heq_config, add_same. cut ((!! config)[pt1] > 0). lia.
             change (In pt1 (!! config)). rewrite <- support_spec, Hsupp. now left.
@@ -482,10 +485,10 @@ destruct Hfmon as [Hfinc | Hfdec].
     - rewrite map_last in Heq. apply Hfinj in Heq. contradiction.
     - intro Habs. apply map_eq_nil in Habs. now apply (sort_non_nil config).
   + rewrite (hd_indep _ (f 0)) in Hneq.
-    - contradiction Hneq. rewrite map_hd. now f_equal.
+    - contradiction Hneq. rewrite map_hd. hnf. now f_equal.
     - intro Habs. apply map_eq_nil in Habs. now apply (sort_non_nil config).
   + rewrite (last_indep _ (f 0)) in Hneq0.
-    - contradiction Hneq0. rewrite map_last. now f_equal.
+    - contradiction Hneq0. rewrite map_last. hnf. now f_equal.
     - intro Habs. apply map_eq_nil in Habs. now apply (sort_non_nil config).
 * repeat Rdec_full; trivial;
   rewrite map_injective_support, (sort_map_decreasing Hfdec) in Heq
@@ -500,10 +503,10 @@ destruct Hfmon as [Hfinc | Hfdec].
     - rewrite last_rev_hd, map_hd in Heq. apply Hfinj in Heq. contradiction.
     - intro Habs. rewrite rev_nil in Habs. apply map_eq_nil in Habs. now apply (sort_non_nil config).
   + rewrite (last_indep _ (f 0)) in Hneq0.
-    - contradiction Hneq0. rewrite last_rev_hd, map_hd. now f_equal.
+    - contradiction Hneq0. rewrite last_rev_hd, map_hd. hnf. now f_equal.
     - intro Habs. rewrite rev_nil in Habs. apply map_eq_nil in Habs. now apply (sort_non_nil config).
   + rewrite (hd_indep _ (f 0)) in Hneq.
-    - contradiction Hneq. rewrite hd_rev_last, map_last. now f_equal.
+    - contradiction Hneq. rewrite hd_rev_last, map_last. hnf. now f_equal.
     - intro Habs. rewrite rev_nil in Habs. apply map_eq_nil in Habs. now apply (sort_non_nil config).
 Qed.
 
@@ -521,7 +524,7 @@ Definition extreme_center (s : observation) := (mini s + maxi s) / 2.
 Instance extreme_center_compat : Proper (equiv ==> eq) extreme_center.
 Proof using . intros s s' Hs. unfold extreme_center, mini, maxi. now rewrite Hs. Qed.
 
-Lemma extreme_center_similarity : forall (sim : similarity location) s, s =/= empty ->
+Lemma extreme_center_similarity : forall (sim : (@similarity location  (@state_Setoid Loc (@location Loc) Info) (@state_EqDec Loc (@location Loc) Info) _ _)) (s:multiset location), s =/= empty ->
   extreme_center (map sim s) = sim (extreme_center s).
 Proof using .
 intros sim s Hs.
@@ -947,16 +950,22 @@ do 2 rewrite obs_from_config_spec, config_list_spec.
 induction names as [| id l]; simpl in *; unfold Datatypes.id in *.
 * reflexivity.
 * changeR. destruct (activate da id).
-  + destruct_match_eq Hext; repeat destruct_match.
+  + changeR. destruct_match_eq Hext;repeat destruct_match.
     - f_equal. apply IHl.
     - apply IHl.
     - contradiction (Rlt_irrefl (mini (!! config))).
+      changeR.
       match goal with H : extreme_center _ == _ |- _ => rewrite <- H at 2 end.
       now apply Generic_min_mid_lt.
     - contradiction (Rlt_irrefl (mini (!! config))).
       match goal with H : extreme_center _ == _ |- _ => rewrite <- H at 2 end.
       now apply Generic_min_mid_lt.
-    - exfalso. revert Hext. unfold is_extremal. repeat destruct_match; tauto || discriminate.
+    - exfalso. revert Hext. unfold is_extremal.
+      rewrite e.
+      repeat destruct_match.
+      -- discriminate.
+      -- discriminate.
+      -- intros _. now apply c0.
     - apply IHl.
   + destruct_match.
     - f_equal. apply IHl.
@@ -984,7 +993,12 @@ induction names as [| id l]; simpl.
     - contradiction (Rlt_irrefl (maxi (!! config))).
       match goal with H : extreme_center _ == _ |- _ => rewrite <- H at 1 end.
       now apply Generic_mid_max_lt.
-    - exfalso. revert Hext. unfold is_extremal. repeat destruct_match; tauto || discriminate.
+    - exfalso. revert Hext. unfold is_extremal.
+      rewrite e.
+      repeat destruct_match;intros ?.
+      -- discriminate.
+      -- discriminate.
+      -- now apply c1.
     - apply IHl.
   + destruct_match.
     - f_equal. apply IHl.
@@ -1118,7 +1132,7 @@ intros config pt. split.
   inversion_clear Hin.
   + subst id'. clear IHl. simpl. hnf in Hroundid. unfold Datatypes.id.
     destruct_match. revert_one @equiv. intro Heq.
-    - rewrite <- Hid in Heq. contradiction Hroundid. now apply WithMultiplicity.no_info.
+    - rewrite <- Hid in Heq. contradiction Hroundid. changeR. now apply WithMultiplicity.no_info.
     - destruct_match; try contradiction; []. apply le_n_S. induction l; simpl.
       -- reflexivity.
       -- repeat destruct_match; try now idtac + apply le_n_S + apply le_S; apply IHl.
@@ -1456,7 +1470,9 @@ Proof using .
 intros config pt Hgather.
 destruct (forallb (fun x => if get_location (config x) =?= pt then true else false) names) eqn:Hall.
 - contradiction Hgather. rewrite forallb_forall in Hall.
-  intro id'. setoid_rewrite Rdec_bool_true_iff in Hall. hnf. repeat rewrite Hall; trivial; apply In_names.
+  intro id'. changeR. 
+  Print Instances Proper.
+  setoid_rewrite Rdec_bool_true_iff in Hall. hnf. repeat rewrite Hall; trivial; apply In_names.
 - rewrite <- negb_true_iff, existsb_forallb, existsb_exists in Hall.
   destruct Hall as [id' [_ Hid']]. revert Hid'. destruct_match; discriminate || intro. now exists id'.
 Qed.
@@ -1510,7 +1526,7 @@ destruct (support (max (!! config))) as [| pt [| pt' l]] eqn:Hmaj.
       assert (Hnodup := support_NoDupA (!! config)).
       rewrite NoDupA_Leibniz, Permuted_sort, Hsup in Hnodup.
       inversion_clear Hnodup. inversion_clear H0. inversion_clear H2.
-      destruct (Rdec pt2 (extreme_center (!! config))) as [Heq | Heq]; subst.
+      destruct (Rdec pt2 (extreme_center (!! config))) as [Heq | Heq]; simpl in Heq;subst.
       - exists pt3. repeat split; try now intro; subst; intuition.
         rewrite <- support_spec, InA_Leibniz, Permuted_sort, Hsup. intuition.
       - exists pt2. repeat split; try now intro; subst; intuition.
diff --git a/CaseStudies/Gathering/InR/Impossibility.v b/CaseStudies/Gathering/InR/Impossibility.v
index 6574320e3499ca01c17e8096138755723e3045b7..a26c70346ae574dcd60a774d8e953f37df75024b 100644
--- a/CaseStudies/Gathering/InR/Impossibility.v
+++ b/CaseStudies/Gathering/InR/Impossibility.v
@@ -23,6 +23,7 @@ Require Import Morphisms.
 Require Import Lia.
 Require Import List SetoidList.
 Require Import Pactole.Util.Preliminary Pactole.Util.Fin.
+Require Import Pactole.Util.Bijection.
 Require Import Pactole.Setting.
 Require Import FMapFacts.
 Require Import Pactole.Spaces.R.
@@ -94,7 +95,7 @@ assert (Heven := even_nG). assert (H0 := nG_non_0).
 simpl. destruct n as [| [| ?]].
 - lia.
 - destruct Heven. lia.
-- simpl. lia.
+- simpl. solve [ auto with arith | lia].
 Qed.
 
 (* We need to unfold [obs_is_ok] for rewriting *)
diff --git a/CaseStudies/Gathering/InR2/Algorithm.v b/CaseStudies/Gathering/InR2/Algorithm.v
index 8d31cd7a9bcf999fc4801f29480e4f7758e7d3d6..c879256a4d315b9cfcce93194c8ea5a0b5856fe6 100644
--- a/CaseStudies/Gathering/InR2/Algorithm.v
+++ b/CaseStudies/Gathering/InR2/Algorithm.v
@@ -36,7 +36,7 @@ Require Export Pactole.Setting.
 (* Specific to R^2 topology *)
 Require Import Pactole.Spaces.R2.
 (* Specific to gathering *)
-Require Pactole.CaseStudies.Gathering.WithMultiplicity.
+Require Import Pactole.CaseStudies.Gathering.WithMultiplicity.
 Require Import Pactole.CaseStudies.Gathering.Definitions.
 (* Specific to multiplicity *)
 Require Import Pactole.Observations.MultisetObservation.
diff --git a/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v b/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
index d413a8550f918c0e594754c18e0555c2d7c8398c..57af3eae0f947e5a5d79407b52f6af0bada36973 100644
--- a/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
+++ b/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
@@ -19,6 +19,7 @@ Require Import RelationPairs.
 Require Import Morphisms.
 Require Import Psatz.
 Require Import Inverse_Image.
+Require Import Pactole.Util.Bijection.
 Require Import Pactole.Setting Pactole.Util.Fin.
 Require Import Pactole.Models.Flexible.
 Require Import Pactole.Models.NoByzantine.
diff --git a/CaseStudies/Gathering/InR2/Peleg.v b/CaseStudies/Gathering/InR2/Peleg.v
index 66a3a761d4336c5caffc33f5eb4f823007b0e617..eba8f8d98228828c3d9318eb99a94599848251d5 100644
--- a/CaseStudies/Gathering/InR2/Peleg.v
+++ b/CaseStudies/Gathering/InR2/Peleg.v
@@ -20,6 +20,7 @@ Require Import Morphisms.
 Require Import Psatz.
 Require Import Inverse_Image.
 Require Import Pactole.Setting.
+Require Import Pactole.Util.Bijection.
 Require Import Pactole.Models.Flexible.
 Require Import Pactole.Models.NoByzantine.
 Require Import Pactole.Observations.MultisetObservation.
diff --git a/CaseStudies/Gathering/WithMultiplicity.v b/CaseStudies/Gathering/WithMultiplicity.v
index 65285e01e3a151afdd6170a30dcea00af5af9b08..e2ca236592e232f6827194b0e38375bcf0b23bb3 100644
--- a/CaseStudies/Gathering/WithMultiplicity.v
+++ b/CaseStudies/Gathering/WithMultiplicity.v
@@ -36,7 +36,7 @@ Section MultisetGathering.
 (** Here, we restrict the state to only contain the location. *)
 Context `{Location}.
 (* TODO: add the existence of a similarity here *)
-Instance Info : State location := OnlyLocation (fun _ => True).
+#[export]Instance Info : State location := OnlyLocation (fun _ => True).
 Context {VS : RealVectorSpace location}.
 Context {RMS : RealMetricSpace location}.
 Context `{Names}.
@@ -46,7 +46,7 @@ Context `{inactive_choice}.
 Context {UpdFun : update_function _ _ _}.
 Context {InaFun : inactive_function _}.
 
-Global Existing Instance multiset_observation.
+#[export] Existing Instance multiset_observation.
 
 Notation "!! config" :=
   (@obs_from_config location _ _ _ multiset_observation config origin : observation) (at level 10).
@@ -143,10 +143,10 @@ destruct Hconfig as [Heven [Hge2 [pt1' [pt2' [Hdiff [Hpt1' Hpt2']]]]]].
 assert (Hcase : pt1' == pt1 /\ pt2' == pt2 \/ pt1' == pt2 /\ pt2' == pt1).
 { assert (Hin1 : InA equiv pt1' (pt1 :: pt2 :: nil)).
   { rewrite <- Hsupp, support_spec. unfold In. rewrite Hpt1'.
-    destruct nG as [| [| nG]]; simpl; lia. }
+    destruct nG as [| [| nG]]; simpl; solve [ auto with arith | lia]. }
   assert (Hin2 : InA equiv pt2' (pt1 :: pt2 :: nil)).
   { rewrite <- Hsupp, support_spec. unfold In. rewrite Hpt2'.
-    destruct nG as [| [| nG]]; simpl; lia. }
+    destruct nG as [| [| nG]]; simpl; solve [ auto with arith | lia]. }
   rewrite 2 InA_cons, InA_nil in Hin1, Hin2. clear -Hin1 Hin2 Hdiff.
   decompose [or] Hin1; decompose [or] Hin2; tauto || contradiction Hdiff; etransitivity; eauto. }
 split.
@@ -212,7 +212,7 @@ destruct (n1 =?= n2) as [Hn | Hn].
 * right.
   intro Hvalid. contradiction Hn.
   assert (Hhalf : 0 < Nat.div2 nG).
-  { destruct Hvalid as [_ [Hle _]]. destruct nG as [| [| ?]]; simpl; lia. }
+  { destruct Hvalid as [_ [Hle _]]. destruct nG as [| [| ?]]; simpl; solve [ auto with arith | lia]. }
   destruct (invalid_strengthen HnB Hvalid) as [pt1' [pt2' Hdiff Hobs]].
   assert (Hperm : PermutationA eq_pair ((pt1, n1) :: (pt2, n2) :: nil)
                                        ((pt1', Nat.div2 nG) :: (pt2', Nat.div2 nG) :: nil)).
diff --git a/CaseStudies/LifeLine/Algorithm.v b/CaseStudies/LifeLine/Algorithm.v
index 633f29acf90c35fe80c8c0094ecc4c5083a00f06..02b9fc67112ff43d8856bc9f68cd56f72d7608ba 100644
--- a/CaseStudies/LifeLine/Algorithm.v
+++ b/CaseStudies/LifeLine/Algorithm.v
@@ -1754,10 +1754,10 @@ destruct (Rlt_dec (fst (tgt_loc x)) (fst (tgt_loc y))).
 Defined.
 
 Instance tgt_lt_compat : Proper (equiv ==> equiv ==> iff) tgt_lt.
-Proof. intros [] [] [] [] [] []. simpl in *. now subst. Qed.
+Proof using. intros [] [] [] [] [] []. simpl in *. now subst. Qed.
 
 Instance tgt_lt_SO : StrictOrder tgt_lt.
-Proof. split.
+Proof using. split.
 + unfold tgt_lt. intros x Habs. decompose [and or] Habs; clear Habs; try congruence; [|];
   eapply (@irreflexivity _ Rlt); eauto; autoclass.
 + unfold tgt_lt. intros x y z Hlt1 Hlt2.
@@ -1791,7 +1791,7 @@ Local Hint Immediate tgt_trichotomy : core.
 Definition choose_min := set_min tgt_lt tgt_lt_dec.
 
 Instance choose_min_compat : Proper (equiv ==> equiv) choose_min.
-Proof. repeat intro. unfold choose_min. apply set_min_compat; autoclass. Qed.
+Proof using. repeat intro. unfold choose_min. apply set_min_compat; autoclass. Qed.
 
 #[refine]
 Instance concrete_params : Param := {|
diff --git a/Core/Formalism.v b/Core/Formalism.v
index 58f1a9f8a1bb2b9f7ffd84be88868b501ae78ec0..19cce23fd7c789375f88e0815c69a8d298aaa2b9 100644
--- a/Core/Formalism.v
+++ b/Core/Formalism.v
@@ -529,7 +529,8 @@ Proof using . intros * Hg. induction Hg; constructor; assumption. Qed.
 Theorem kFair_Fair : forall k (d : demon), kFair k d -> Fair d.
 Proof using .
 intro. apply Stream.forever_impl_compat.
-intros ? ? id. eauto using (@Between_eventually_activated id _ id).
+intros ? ? id.
+eapply (@Between_eventually_activated id _ id);eauto.
 Qed.
 
 (** [Between g h d k] is monotonic on [k]. *)
diff --git a/Makefile.local b/Makefile.local
index 35c1d6bf68c70f9582e0935d89f1754b65b65684..060b3d563d3f0159cf4d3dbcd34f7f7223355165 100644
--- a/Makefile.local
+++ b/Makefile.local
@@ -34,15 +34,23 @@ vok-nocheck: $(VOKFILESNOASSUMPTION)
 # 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 -deprecated-instance-without-locality
 #COQEXTRAFLAGS+= -w -intuition-auto-with-star
 #COQEXTRAFLAGS+= -w -argument-scope-delimiter
-#COQEXTRAFLAGS+= -w -deprecated-syntactic-definition
+COQEXTRAFLAGS+= -w -deprecated-syntactic-definition
 #COQEXTRAFLAGS+= -w -future-coercion-class-field
 
 
 core: Pactole_all.vo
 
+# make ../foo.check Ask to compile foo.v id necessary and then coqchk foo.vo
+%.check: %.vo
+	$(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $<
+
+# make ../foo.v displays the dependencies of foo.v
+%.dep: %.v
+	$(TIMER) $(COQDEP) $(COQLIBS) $<
+
 recore:
 	dev/rebuild_pactole_all.sh > Pactole_all.v
 	make Pactole_all.vo
diff --git a/Models/GraphEquivalence.v b/Models/GraphEquivalence.v
index 231d86a1dbde08d047b2a374bd091baa805e50c2..7236135f150823c3ff07ab604c51ba49f3c833d9 100644
--- a/Models/GraphEquivalence.v
+++ b/Models/GraphEquivalence.v
@@ -17,6 +17,7 @@ Require Import Reals.
 Require Import Psatz.
 Require Import SetoidList.
 
+Require Import Pactole.Util.Bijection.
 Require Import Pactole.Setting.
 Require Import Pactole.Spaces.Graph.
 Require Import Pactole.Spaces.Isomorphism.
@@ -24,6 +25,52 @@ Require Import Pactole.Spaces.ThresholdIsomorphism.
 Require Import Pactole.Models.ContinuousGraph.
 Require Import Pactole.Models.DiscreteGraph.
 
+#[local]
+Hint Extern 9 (_ = _ :>nat) => lia: zarith.
+#[local]
+Hint Extern 9 (_ <= _) => lia: zarith.
+#[local]
+Hint Extern 9 (_ < _) => lia: zarith.
+#[local]
+Hint Extern 9 (_ >= _) => lia: zarith.
+#[local]
+Hint Extern 9 (_ > _) => lia: zarith.
+
+#[local]
+Hint Extern 9 (_ <> _ :>nat) => lia: zarith.
+#[local]
+Hint Extern 9 (~ _ <= _) => lia: zarith.
+#[local]
+Hint Extern 9 (~ _ < _) => lia: zarith.
+#[local]
+Hint Extern 9 (~ _ >= _) => lia: zarith.
+#[local]
+Hint Extern 9 (~ _ > _) => lia: zarith.
+
+#[local]
+Hint Extern 9 (_ = _ :>Z) => lia: zarith.
+#[local]
+Hint Extern 9 (_ <= _)%Z => lia: zarith.
+#[local]
+Hint Extern 9 (_ < _)%Z => lia: zarith.
+#[local]
+Hint Extern 9 (_ >= _)%Z => lia: zarith.
+#[local]
+Hint Extern 9 (_ > _)%Z => lia: zarith.
+
+#[local]
+Hint Extern 9 (_ <> _ :>Z) => lia: zarith.
+#[local]
+Hint Extern 9 (~ (_ <= _)%Z) => lia: zarith.
+#[local]
+Hint Extern 9 (~ (_ < _)%Z) => lia: zarith.
+#[local]
+Hint Extern 9 (~ (_ >= _)%Z) => lia: zarith.
+#[local]
+Hint Extern 9 (~ (_ > _)%Z) => lia: zarith.
+
+#[local]
+Hint Extern 9 False => lia: zarith.
 
 (* Typeclasses eauto := (bfs). *)
 Open Scope R_scope.
@@ -680,18 +727,13 @@ simpl activate. destruct_match_eq Hactive.
       (* cut ((bijectionG Ciso' (OnEdge e (1 /sr 2))) == (bijectionG (inverse Ciso) (OnEdge e (1 /sr 2)))). *)
       pose (hsim := @bijectionG V E TG (inverse Ciso)).
 
-      assert (@equiv loc locG_Setoid
+      assert (@equiv (@loc V E TG) locG_Setoid
                 (@bijectionG V E TG Ciso' (@OnEdge V E TG e (1 /sr 2)))
                 (@hsim (@OnEdge V E TG e (1 /sr 2)) )).
-      { rewrite <- (HCf (OnEdge e (1 /sr 2))).
+      { rewrite <- (HCf (@OnEdge V E TG e (1 /sr 2))).
         reflexivity. }
       destruct H.
-      assumption.
-
-      (* 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. *)
-    }
+      assumption. }
     assert (HnotOnEdge : forall e p, Clocal_config (Good g) =/= SOnEdge e p).
     { intros e0 p0 H0.
       destruct (Clocal_config (Good g)) as [| e p] eqn:Habs; try tauto; [].
diff --git a/Models/RigidFlexibleEquivalence.v b/Models/RigidFlexibleEquivalence.v
index 98077dfc007a5408192e0eb40fb067ca5344c780..282b2cee0a9ba43d9016bd55b9649ea7b742c837 100644
--- a/Models/RigidFlexibleEquivalence.v
+++ b/Models/RigidFlexibleEquivalence.v
@@ -24,6 +24,7 @@ Require Import Reals Psatz.
 Require Import Pactole.Setting.
 Require Import Pactole.Spaces.RealMetricSpace.
 Require Import Pactole.Spaces.Similarity.
+Require Import Pactole.Util.Bijection.
 Require Pactole.Models.Rigid.
 Require Pactole.Models.Flexible.
 
diff --git a/Observations/LimitedMultisetObservation.v b/Observations/LimitedMultisetObservation.v
index ee35ad67c2aa44532d5ff1d3185e78c0b8d1bbae..2fc98cc07d6b32a2ca64ab901160daad01972440 100644
--- a/Observations/LimitedMultisetObservation.v
+++ b/Observations/LimitedMultisetObservation.v
@@ -23,6 +23,7 @@ Require Import Lia.
 Require Import SetoidList.
 Require Import SetoidDec.
 Require Import Rbase.
+Require Import Pactole.Util.Bijection.
 Require Import Pactole.Util.FMaps.FMapList.
 Require Import Pactole.Util.MMultiset.MMultisetWMap.
 Require Export Pactole.Util.MMultiset.MMultisetInterface.
@@ -41,8 +42,6 @@ Require Import Pactole.Spaces.Similarity.
 Close Scope R_scope.
 Set Implicit Arguments.
 
-Coercion Bijection.section : Bijection.bijection >-> Funclass.
-
 
 Section MultisetObservation.
 
diff --git a/Observations/LimitedSetObservation.v b/Observations/LimitedSetObservation.v
index d530d54229535d5f68e4898e2d7740b297ff1145..d147a81de8f3742089e2b852481e86df171531da 100644
--- a/Observations/LimitedSetObservation.v
+++ b/Observations/LimitedSetObservation.v
@@ -22,6 +22,7 @@ Require Import SetoidDec.
 Require Import Rbase.
 Require Import Pactole.Util.FSets.FSetInterface.
 Require Import Pactole.Util.FSets.FSetFacts.
+Require Import Pactole.Util.Bijection.
 Require Import Pactole.Util.Coqlib.
 Require Import Pactole.Core.Identifiers.
 Require Import Pactole.Core.State.
@@ -30,7 +31,6 @@ Require Import Pactole.Observations.Definition.
 Require Import Pactole.Spaces.RealMetricSpace.
 Require Import Pactole.Spaces.Similarity.
 Require Pactole.Observations.SetObservation.
-Coercion Bijection.section : Bijection.bijection >-> Funclass.
 
 
 Section LimitedSetObservation.
@@ -75,7 +75,7 @@ Lemma obs_from_config_map : forall radius (sim : similarity location),
 Proof using .
 repeat intro. unfold obs_from_config, limited_set_observation.
 rewrite config_list_map; try (now apply lift_compat; simpl; apply Bijection.section_compat); [].
-rewrite map_map, 2 filter_map, <- SetObservation.make_set_map, map_map; autoclass; [].
+rewrite map_map, 2 filter_map, <- SetObservation.make_set_map, map_map; autoclass.
 apply SetObservation.make_set_compat, eqlistA_PermutationA_subrelation.
 assert (Hequiv : (@equiv _ state_Setoid ==> @equiv _ location_Setoid)%signature
           (fun x => sim (get_location x)) (fun x => get_location (lift (existT precondition sim Psim) x))).
diff --git a/Spaces/Grid.v b/Spaces/Grid.v
index 943409ba52088b1c328867503692643873fa6210..4b6c7aa433efc52500211ec6360f9dadb4055d10 100644
--- a/Spaces/Grid.v
+++ b/Spaces/Grid.v
@@ -11,6 +11,7 @@
 
 Require Import Psatz SetoidDec ZArith Rbase.
 Require Import Pactole.Util.Coqlib.
+Require Import Pactole.Util.Bijection.
 Require Export Pactole.Spaces.Graph.
 
 
@@ -23,9 +24,9 @@ Open Scope Z_scope.
 Inductive direction :=
   North | South | East | West | Self.
 
-Global Instance direction_Setoid : Setoid direction := eq_setoid _.
+#[export] Instance direction_Setoid : Setoid direction := eq_setoid _.
 
-Global Instance direction_EqDec : EqDec direction_Setoid.
+#[export] Instance direction_EqDec : EqDec direction_Setoid.
 Proof using .
 intros x y. simpl. change (x = y -> False) with (x <> y). decide equality.
 Defined.
@@ -34,8 +35,8 @@ Defined.
 Notation node := (Z*Z)%type.
 Notation edge := (Z*Z*direction)%type.
 
-Global Instance node_Setoid : Setoid node := eq_setoid _.
-Global Instance node_EqDec : EqDec node_Setoid.
+#[export] Instance node_Setoid : Setoid node := eq_setoid _.
+#[export] Instance node_EqDec : EqDec node_Setoid.
 Proof using .
 intros x y.
 destruct (fst x =?= fst y).
@@ -45,8 +46,8 @@ destruct (fst x =?= fst y).
 + right. abstract (destruct x, y; injection; auto).
 Defined.
 
-Global Instance edge_Setoid : Setoid edge := eq_setoid _.
-Global Instance edge_EqDec : EqDec edge_Setoid.
+#[export] Instance edge_Setoid : Setoid edge := eq_setoid _.
+#[export] Instance edge_EqDec : EqDec edge_Setoid.
 Proof using .
 intros x y.
 destruct (fst x =?= fst y).
@@ -67,7 +68,7 @@ Definition edge_tgt (e : edge) : node :=
 Arguments edge_tgt !e.
 
 (** The Z² grid is a graph. *)
-Global Instance Z2 : Graph node edge.
+#[export] Instance Z2 : Graph node edge.
 simple refine {| V_EqDec := node_EqDec;
                  E_EqDec := edge_EqDec;
                  src := fst;
@@ -93,13 +94,13 @@ Require Pactole.Util.Bijection.
 Require Import Pactole.Core.State.
 Require Import Pactole.Core.Formalism.
 
-Global Instance Loc : Location := {| location := node |}.
+#[export] Instance Loc : Location := {| location := node |}.
 (** angle: anglei represents the possible angles for a rotation of reflection:
     - for a rotation: angle i/2 * pi;
     - for a reflection: angle i/4 * pi *)
 Inductive angle := angle0 | angle1 | angle2 | angle3.
-Global Instance angle_Setoid : Setoid angle := eq_setoid _.
-Global Instance angle_EqDec : EqDec angle_Setoid.
+#[export] Instance angle_Setoid : Setoid angle := eq_setoid _.
+#[export] Instance angle_EqDec : EqDec angle_Setoid.
 Proof using .
 intros x y. simpl.
 change (x = y -> False) with (x <> y).
@@ -125,7 +126,7 @@ intros x y. simpl.
 abstract (split; intro; subst; destruct x || destruct y; f_equal; simpl; lia).
 Defined.
 
-Global Instance translation_compat : Proper (equiv ==> equiv) translation.
+#[export] Instance translation_compat : Proper (equiv ==> equiv) translation.
 Proof. intros ? ? Heq x. Fail timeout 2 now rewrite Heq. cbn in Heq. now subst. Qed.
 
 (** Rotation *)
@@ -149,7 +150,7 @@ intros x y. cbn.
 abstract (split; intro; subst; destruct r; cbn; destruct x || destruct y; cbn; f_equal; lia).
 Defined.
 
-(* Global Instance rotation_compat : Proper (equiv ==> equiv) rotation := reflexive_proper _. *)
+(* #[export] Instance rotation_compat : Proper (equiv ==> equiv) rotation := reflexive_proper _. *)
 
 (** Reflection *)
 Definition mk_reflection r : Z*Z -> Z*Z :=
@@ -172,28 +173,28 @@ intros x y. cbn.
 abstract (split; intro; subst; destruct r; cbn; destruct x || destruct y; cbn; f_equal; lia).
 Defined.
 
-(* Global Instance reflection_compat : Proper (equiv ==> equiv) reflection := reflexive_proper _. *)
+(* #[export] Instance reflection_compat : Proper (equiv ==> equiv) reflection := reflexive_proper _. *)
 
 (** ***  Change of frame of reference  **)
 
 (** Translation  **)
-Global Instance FCTranslation : frame_choice (Z*Z) := {|
+#[export] Instance FCTranslation : frame_choice (Z*Z) := {|
   frame_choice_bijection := translation;
   frame_choice_Setoid := _;
   frame_choice_bijection_compat := _ |}.
 
 (** Rigid Motion  **)
-Global Instance rigid_motion_compat :
+#[export] Instance rigid_motion_compat :
   Proper (equiv ==> equiv) (fun rm => rotation (snd rm) ∘ translation (fst rm)).
 Proof using . intros ? ? [Hv Ha]; do 2 f_equiv; assumption. Qed.
 
-Global Instance FCRigidMotion : frame_choice (Z*Z*angle) := {|
+#[export] Instance FCRigidMotion : frame_choice (Z*Z*angle) := {|
   frame_choice_bijection := fun rm => rotation (snd rm) ∘ translation (fst rm);
   frame_choice_Setoid := prod_Setoid node_Setoid angle_Setoid;
   frame_choice_bijection_compat := rigid_motion_compat |}.
 
 (** Similarities *)
-Global Instance FCSimilarity : frame_choice (bool*(Z*Z)*angle)%type.
+#[export] Instance FCSimilarity : frame_choice (bool*(Z*Z)*angle)%type.
 simple refine {|
   frame_choice_bijection := fun '(b, v, a) =>
    rotation a ∘ translation v ∘ (if b : bool then reflection angle0 else @Bijection.id node _);
diff --git a/Spaces/R2.v b/Spaces/R2.v
index 6eff916ba6e9e3c560101f449d2f516e7b7f6f21..ca086f9ee3a30da67d024c6ff5dc0a6a4d80302a 100644
--- a/Spaces/R2.v
+++ b/Spaces/R2.v
@@ -26,11 +26,11 @@ Import List Permutation SetoidList.
 Require Import SetoidDec.
 Require Import FunInd.
 Require Import Pactole.Util.Coqlib.
+Require Import Pactole.Util.Bijection.
 Require Export Pactole.Spaces.EuclideanSpace.
 Require Import Pactole.Spaces.Similarity.
 Set Implicit Arguments.
 Open Scope R_scope.
-Coercion Bijection.section : Bijection.bijection >-> Funclass.
 
 
 (** **  R² as a Euclidean space over R  **)
diff --git a/Util/Bijection.v b/Util/Bijection.v
index 5d8b1ec72c1a099d17e4789c046b344f85e28195..a7ed108b9a9e59b441049fe638bcd1a1ea30d343 100644
--- a/Util/Bijection.v
+++ b/Util/Bijection.v
@@ -30,9 +30,9 @@ Record bijection := {
   retraction : T → T;
   section_compat : Proper (equiv ==> equiv) section;
   Inversion : ∀ x y, section x == y ↔ retraction y == x}.
-Global Existing Instance section_compat.
+#[export]Existing Instance section_compat.
 
-Global Instance bij_Setoid : Setoid bijection.
+#[export]Instance bij_Setoid : Setoid bijection.
 simple refine {| equiv := λ f g, ∀ x, f.(section) x == g x |}; auto; [].
 Proof. split.
 + repeat intro. reflexivity.
@@ -41,14 +41,14 @@ Proof. split.
 Defined.
 
 (* Use fun_Setoid directly in the definition of bij_Setoid? *)
-Global Instance bij_Setoid_eq_compat : Proper ((@equiv bijection bij_Setoid)
+#[export]Instance bij_Setoid_eq_compat : Proper ((@equiv bijection bij_Setoid)
   ==> (@equiv (T -> T) (fun_Setoid T HeqT))) section.
 Proof using . intros ?? H. apply H. Qed.
 
-Global Instance section_full_compat : Proper (equiv ==> (equiv ==> equiv)) section.
+#[export]Instance section_full_compat : Proper (equiv ==> (equiv ==> equiv)) section.
 Proof using . intros f g Hfg x y Hxy. rewrite Hxy. now apply Hfg. Qed.
 
-Global Instance retraction_compat : Proper (equiv ==> (equiv ==> equiv)) retraction.
+#[export]Instance retraction_compat : Proper (equiv ==> (equiv ==> equiv)) retraction.
 Proof using . intros f g Hfg x y Hxy. now rewrite <- f.(Inversion), Hxy, Hfg, g.(Inversion). Qed.
 
 (** The identity bijection *)
@@ -67,7 +67,7 @@ Proof.
 + abstract (intros x y; now rewrite f.(Inversion), <- g.(Inversion)).
 Defined.
 
-Global Instance BijectionComposition : Composition bijection.
+#[export]Instance BijectionComposition : Composition bijection.
 refine {| compose := comp |}.
 Proof.
 intros f1 f2 Hf g1 g2 Hg x. cbn -[equiv].
@@ -78,7 +78,7 @@ Lemma compE : ∀ f g : bijection, f ∘ g = (λ t, f (g t)) :> (T -> T).
 Proof using . reflexivity. Qed.
 
 (*
-Global Instance compose_compat : Proper (equiv ==> equiv ==> equiv) compose.
+#[export]Instance compose_compat : Proper (equiv ==> equiv ==> equiv) compose.
 Proof.
 intros f1 f2 Hf g1 g2 Hg x. cbn -[equiv].
 rewrite (Hf (g1 x)). f_equiv. apply Hg.
@@ -93,7 +93,7 @@ refine {| section := bij.(retraction);
           retraction := bij.(section) |}.
 Proof. abstract (intros; rewrite bij.(Inversion); reflexivity). Defined.
 
-Global Instance BijectionInverse : Inverse bijection.
+#[export]Instance BijectionInverse : Inverse bijection.
 refine {| inverse := inv |}.
 Proof. repeat intro. simpl. now f_equiv. Defined.
 
@@ -110,7 +110,7 @@ Lemma inv_inv : ∀ b : bijection, b⁻¹⁻¹ == b.
 Proof using . intros. cbn. reflexivity. Qed.
 
 (*
-Global Instance inverse_compat : Proper (equiv ==> equiv) inverse.
+#[export]Instance inverse_compat : Proper (equiv ==> equiv) inverse.
 Proof. repeat intro. simpl. now f_equiv. Qed.
 *)
 Lemma retraction_section : forall (bij : bijection) x, bij.(retraction) (bij.(section) x) == x.
@@ -172,7 +172,7 @@ Lemma prod_bijVE : ∀ (BA : bijection A) (BB : bijection B),
   prod_bij BA BB⁻¹ = (λ p, (BA⁻¹ (fst p), BB⁻¹ (snd p))) :> (A * B -> A * B).
 Proof using . reflexivity. Qed.
 
-Global Instance prod_bij_compat : Proper (equiv ==> equiv ==> equiv) prod_bij.
+#[export]Instance prod_bij_compat : Proper (equiv ==> equiv ==> equiv) prod_bij.
 Proof using .
   intros * BA1 BA2 HA BB1 BB2 HB p. rewrite 2 prod_bijE. split.
   rewrite HA. reflexivity. rewrite HB. reflexivity.
@@ -208,7 +208,7 @@ Lemma prod_eq_bijVE : ∀ (BA : bijection A) (BB : bijection B),
   prod_eq_bij BA BB⁻¹ = (λ p, (BA⁻¹ (fst p), BB⁻¹ (snd p))) :> (A * B -> A * B).
 Proof using . reflexivity. Qed.
 
-Global Instance prod_eq_bij_compat :
+#[export]Instance prod_eq_bij_compat :
   Proper (equiv ==> equiv ==> equiv) prod_eq_bij.
 Proof using .
   cbn. intros * BA1 BA2 HA BB1 BB2 HB p. rewrite 2 prod_eq_bijE, <- pair_eqE.
diff --git a/Util/FMaps/FMapFacts.v b/Util/FMaps/FMapFacts.v
index 4a7d9376a32859cb871f954f902e3a6aa3bf5ac2..f2241b0e1e9252198e19242ed80c76c804b9b434 100644
--- a/Util/FMaps/FMapFacts.v
+++ b/Util/FMaps/FMapFacts.v
@@ -68,7 +68,7 @@ Section WeakFacts.
     Lemma MapsTo_iff : forall m x y e, x == y ->
       (MapsTo x e m <-> MapsTo y e m).
     Proof using HF.
-      split; apply MapsTo_1; auto using symmetry.
+      split; apply MapsTo_1 ; auto (*using symmetry stopped working/being useful in 8.20*).
     Qed.
 
     Lemma mem_in_iff : forall m x, In x m <-> mem x m = true.
diff --git a/Util/FSets/FSetFacts.v b/Util/FSets/FSetFacts.v
index 62a1805487af8fcad42e473a02672d893ed965c2..1fc67182a3326171d6b4cfa01a046b0863cc6f20 100644
--- a/Util/FSets/FSetFacts.v
+++ b/Util/FSets/FSetFacts.v
@@ -71,7 +71,7 @@ Section IffSpec.
     split; [| destruct 1; [apply add_1 | apply add_2]]; auto.
     destruct (Helt x y) as [E|E].
     - intro. auto.
-    - intro H; right. eauto using add_3.
+    - intro H; right. eapply add_3;eauto. (* stopped working eauto using eauto *)
   Qed.
 
   Lemma add_other : x =/= y -> (In y (add x s) <-> In y s).
diff --git a/Util/MMultiset/MMultisetExtraOps.v b/Util/MMultiset/MMultisetExtraOps.v
index 1b3cc0b88a72be46d09f0dc5ed5d7ad7bd678163..df83277bc5452cb24281eb631e066c11b5237166 100644
--- a/Util/MMultiset/MMultisetExtraOps.v
+++ b/Util/MMultiset/MMultisetExtraOps.v
@@ -14,6 +14,7 @@ Require Import SetoidList.
 Require Import RelationPairs.
 Require Import SetoidDec.
 
+Require Import Pactole.Util.SetoidDefs.
 Require Import Pactole.Util.MMultiset.Preliminary.
 Require Import Pactole.Util.MMultiset.MMultisetInterface.
 Require Import Pactole.Util.MMultiset.MMultisetFacts.
diff --git a/Util/MMultiset/MMultisetWMap.v b/Util/MMultiset/MMultisetWMap.v
index 0bae9d083dd33dba43774433ed50c877dd1f5385..184c77860ef5314baa4bed947ff3df651dfb7e8a 100644
--- a/Util/MMultiset/MMultisetWMap.v
+++ b/Util/MMultiset/MMultisetWMap.v
@@ -20,6 +20,7 @@ Require Import Pactole.Util.FMaps.FMapInterface.
 Require Import Pactole.Util.FMaps.FMapFacts.
 Require Import Pactole.Util.MMultiset.Preliminary.
 Require Import Pactole.Util.MMultiset.MMultisetInterface.
+Require Import Pactole.Util.SetoidDefs.
 Require Import SetoidDec.
 
 
diff --git a/Util/NumberComplements.v b/Util/NumberComplements.v
index cd13e26dfad28438886b646a6245dd22f36f4c08..ae022b589c53129db4c6cf69afbc98e03c6bcc2c 100644
--- a/Util/NumberComplements.v
+++ b/Util/NumberComplements.v
@@ -50,15 +50,9 @@ Proof. split.
 + intros ? ? ?. apply Rlt_trans.
 Qed.
 
-Lemma Rdec : forall x y : R, {x = y} + {x <> y}.
-Proof.
-intros x y. destruct (Rle_dec x y). destruct (Rle_dec y x).
-  left. now apply Rle_antisym.
-  right; intro; subst. contradiction.
-  right; intro; subst. pose (Rle_refl y). contradiction.
-Qed.
-
-Global Instance R_EqDec : @EqDec R _ := Rdec.
+Global Instance R_EqDec : @EqDec R _ := Req_dec_T.
+(* #[export]  *)
+Notation Rdec := R_EqDec.
 
 Lemma Rdiv_le_0_compat : forall a b, 0 <= a -> 0 < b -> 0 <= a / b.
 Proof. intros a b ? ?. now apply Fourier_util.Rle_mult_inv_pos. Qed.
diff --git a/Util/Preliminary.v b/Util/Preliminary.v
index 0842f1c53153889cd350cdfb257d8e187fb9a3f6..5a579429aa0606cad4205eefc98496071e9d3c8d 100644
--- a/Util/Preliminary.v
+++ b/Util/Preliminary.v
@@ -81,7 +81,7 @@ Definition monotonic {A B : Type} (RA : relation A) (RB : relation B) (f : A ->
 
 Definition full_relation {A : Type} := fun _ _ : A => True.
 
-Global Hint Extern 0 (full_relation _ _) => exact I : core.
+#[export] Hint Extern 0 (full_relation _ _) => exact I : core.
 
 Global Instance relation_equivalence_subrelation {A} :
   forall R R' : relation A, relation_equivalence R R' -> subrelation R R'.
diff --git a/Util/SetoidDefs.v b/Util/SetoidDefs.v
index 7119f42a75e6aa5b72e335320c01282f207bcc80..7308e14c9e63574c2ae9873dc518588678f34624 100644
--- a/Util/SetoidDefs.v
+++ b/Util/SetoidDefs.v
@@ -27,19 +27,19 @@ Set Implicit Arguments.
 (* To avoid infinite loops, we use a breadth-first search... *)
 Typeclasses eauto := (bfs) 20.
 (* but we need to remove [eq_setoid] as it matches everything... *)
-Global Remove Hints eq_setoid : Setoid.
+#[export] Remove Hints eq_setoid : Setoid.
 (* while still declaring it for the types for which we still want to use it. *)
-Global Instance R_Setoid : Setoid R := eq_setoid R.
-Global Instance Z_Setoid : Setoid Z := eq_setoid Z.
-Global Instance nat_Setoid : Setoid nat := eq_setoid nat.
-Global Instance bool_Setoid : Setoid bool := eq_setoid bool.
-Global Instance unit_Setoid : Setoid unit := eq_setoid unit.
-
-Global Instance R_EqDec : EqDec R_Setoid := Req_EM_T.
-Global Instance Z_EqDec : EqDec Z_Setoid := Z.eq_dec.
-Global Instance nat_EqDec : EqDec nat_Setoid := Nat.eq_dec.
-Global Instance bool_EqDec : EqDec bool_Setoid := Bool.bool_dec.
-Global Instance unit_EqDec : EqDec unit_Setoid := fun x y => match x, y with tt, tt => left eq_refl end.
+#[export]Instance R_Setoid : Setoid R := eq_setoid R.
+#[export]Instance Z_Setoid : Setoid Z := eq_setoid Z.
+#[export]Instance nat_Setoid : Setoid nat := eq_setoid nat.
+#[export]Instance bool_Setoid : Setoid bool := eq_setoid bool.
+#[export]Instance unit_Setoid : Setoid unit := eq_setoid unit.
+
+#[export]Instance R_EqDec : EqDec R_Setoid := Req_dec_T.
+#[export]Instance Z_EqDec : EqDec Z_Setoid := Z.eq_dec.
+#[export]Instance nat_EqDec : EqDec nat_Setoid := Nat.eq_dec.
+#[export]Instance bool_EqDec : EqDec bool_Setoid := Bool.bool_dec.
+#[export]Instance unit_EqDec : EqDec unit_Setoid := fun x y => match x, y with tt, tt => left eq_refl end.
 
 Notation "x == y" := (equiv x y).
 Notation "x == y :> A" := (@equiv A _ x y) (at level 70, y at next level, no associativity, only parsing).
@@ -52,7 +52,7 @@ Proof using . intros. destruct_match; intuition auto with *. Qed.
 
 (** **  Setoid Definitions  **)
 
-Global Instance fun_Setoid A B `(Setoid B) : Setoid (A -> B) | 4.
+Instance fun_Setoid A B `(Setoid B) : Setoid (A -> B) | 4.
 Proof. exists (fun f g : A -> B => forall x, f x == g x).
 split.
 + repeat intro. reflexivity.
@@ -60,20 +60,20 @@ split.
 + repeat intro. etransitivity; eauto.
 Defined.
 
-Global Instance fun_Setoid_respectful_compat (A B : Type) (SB : Setoid B) :
+#[export]Instance fun_Setoid_respectful_compat (A B : Type) (SB : Setoid B) :
   subrelation (@equiv (A->B) (fun_Setoid A SB))
     (respectful (@eq A) (@equiv B SB)).
 Proof using . intros ?? H ???. subst. apply H. Qed.
 
-Global Instance fun_Setoid_pointwise_compat A B `{Setoid B} :
+#[export]Instance fun_Setoid_pointwise_compat A B `{Setoid B} :
   subrelation (@equiv _ (fun_Setoid A _)) (pointwise_relation _ equiv).
 Proof using . intros f g Hfg x. apply Hfg. Qed.
 
-Global Instance eq_Setoid_eq_compat (T : Type) :
+#[export]Instance eq_Setoid_eq_compat (T : Type) :
   subrelation (@equiv T (eq_setoid T)) (@eq T).
 Proof using . apply subrelation_refl. Qed.
 
-Global Instance eq_eq_Setoid_compat (T : Type) :
+#[export]Instance eq_eq_Setoid_compat (T : Type) :
   subrelation (@eq T) (@equiv T (eq_setoid T)).
 Proof using . apply subrelation_refl. Qed.
 
@@ -87,21 +87,21 @@ Definition opt_eq {T} (eqT : T -> T -> Prop) (xo yo : option T) :=
     | Some x, Some y => eqT x y
   end.
 
-Global Instance opt_eq_refl : ∀ T (R : T -> T -> Prop), Reflexive R -> Reflexive (opt_eq R).
+#[export]Instance opt_eq_refl : ∀ T (R : T -> T -> Prop), Reflexive R -> Reflexive (opt_eq R).
 Proof using . intros T R HR [x |]; simpl; auto. Qed.
 
-Global Instance opt_eq_sym : ∀ T (R : T -> T -> Prop), Symmetric R -> Symmetric (opt_eq R).
+#[export]Instance opt_eq_sym : ∀ T (R : T -> T -> Prop), Symmetric R -> Symmetric (opt_eq R).
 Proof using . intros T R HR [x |] [y |]; simpl; auto. Qed.
 
-Global Instance opt_eq_trans : ∀ T (R : T -> T -> Prop), Transitive R -> Transitive (opt_eq R).
+#[export]Instance opt_eq_trans : ∀ T (R : T -> T -> Prop), Transitive R -> Transitive (opt_eq R).
 Proof using . intros T R HR [x |] [y |] [z |]; simpl; intros; eauto; contradiction. Qed.
 
-Global Instance opt_equiv T eqT (HeqT : @Equivalence T eqT) : Equivalence (opt_eq eqT).
+#[export]Instance opt_equiv T eqT (HeqT : @Equivalence T eqT) : Equivalence (opt_eq eqT).
 Proof using . split; auto with typeclass_instances. Qed.
 
-Global Instance opt_Setoid T (S : Setoid T) : Setoid (option T) := {| equiv := opt_eq equiv |}.
+#[export]Instance opt_Setoid T (S : Setoid T) : Setoid (option T) := {| equiv := opt_eq equiv |}.
 
-Global Instance Some_compat `(Setoid) : Proper (equiv ==> @equiv _ (opt_Setoid _)) Some.
+#[export]Instance Some_compat `(Setoid) : Proper (equiv ==> @equiv _ (opt_Setoid _)) Some.
 Proof using . intros ? ? Heq. apply Heq. Qed.
 
 Lemma Some_inj {T : Type} {ST : Setoid T} :
@@ -165,7 +165,7 @@ Qed.
 (* This Setoid could be written using RelProd in which case,
    revealing the "and" inside would be more troublesome than
    with this simple definition. *)
-Global Instance prod_Setoid A B (SA : Setoid A) (SB : Setoid B) : Setoid (A * B).
+#[export]Instance prod_Setoid A B (SA : Setoid A) (SB : Setoid B) : Setoid (A * B).
 simple refine {| equiv := fun xn yp => fst xn == fst yp /\ snd xn == snd yp |}; auto; [].
 Proof. split.
 + repeat intro; now split.
@@ -173,7 +173,7 @@ Proof. split.
 + intros ? ? ? [? ?] [? ?]; split; etransitivity; eauto.
 Defined.
 
-Global Instance prod_EqDec A B (SA : Setoid A) (SB : Setoid B) (EDA : EqDec SA) (EDB : EqDec SB)
+#[export]Instance prod_EqDec A B (SA : Setoid A) (SB : Setoid B) (EDA : EqDec SA) (EDB : EqDec SB)
   : EqDec (prod_Setoid SA SB).
 refine (fun xn yp => if equiv_dec (fst xn) (fst yp) then
                      if equiv_dec (snd xn) (snd yp) then left _ else right _
@@ -184,15 +184,15 @@ Proof.
 - abstract (intros [? ?]; contradiction).
 Defined.
 
-Global Instance fst_compat (A B : Type) (SA : Setoid A) (SB : Setoid B) :
+#[export]Instance fst_compat (A B : Type) (SA : Setoid A) (SB : Setoid B) :
   Proper (@equiv (A*B) (prod_Setoid SA SB) ==> @equiv A SA) fst.
 Proof using . intros ?? [H _]. exact H. Qed.
 
-Global Instance snd_compat (A B : Type) (SA : Setoid A) (SB : Setoid B) :
+#[export]Instance snd_compat (A B : Type) (SA : Setoid A) (SB : Setoid B) :
   Proper (@equiv (A*B) (prod_Setoid SA SB) ==> @equiv B SB) snd.
 Proof using . intros ?? [_ H]. exact H. Qed.
 
-Global Instance pair_compat (A B : Type) (SA : Setoid A) (SB : Setoid B) :
+#[export]Instance pair_compat (A B : Type) (SA : Setoid A) (SB : Setoid B) :
   Proper (@equiv A SA ==> @equiv B SB ==> @equiv (A*B) (prod_Setoid SA SB)) pair.
 Proof using . intros ?? Hf ?? Hs. split; cbn. exact Hf. exact Hs. Qed.
 
@@ -205,7 +205,7 @@ Proof using .
 Qed.
 
 (* Setoid over [sig] types *)
-Global Instance sig_Setoid {T} (S : Setoid T) {P : T -> Prop} : Setoid (sig P).
+#[export]Instance sig_Setoid {T} (S : Setoid T) {P : T -> Prop} : Setoid (sig P).
 simple refine {| equiv := fun x y => proj1_sig x == proj1_sig y |}; auto; [].
 Proof. split.
 + intro. reflexivity.
@@ -213,10 +213,10 @@ Proof. split.
 + intros ? ? ? ? ?. etransitivity; eauto.
 Defined.
 
-Global Instance sig_EqDec {T} {S : Setoid T} (E : EqDec S) (P : T -> Prop) : EqDec (@sig_Setoid T S P).
+#[export]Instance sig_EqDec {T} {S : Setoid T} (E : EqDec S) (P : T -> Prop) : EqDec (@sig_Setoid T S P).
 Proof. intros ? ?. simpl. apply equiv_dec. Defined.
 
-Global Instance proj1_sig_compat {T} {S : Setoid T} (E : EqDec S) (P : T -> Prop) :
+#[export]Instance proj1_sig_compat {T} {S : Setoid T} (E : EqDec S) (P : T -> Prop) :
   Proper (@equiv _ (sig_Setoid S) ==> equiv) (@proj1_sig T P).
 Proof using . intros ?? H. apply H. Qed.
 
@@ -224,7 +224,7 @@ Lemma proj1_sig_inj : ∀ {T : Type} {S : Setoid T} (P : T -> Prop),
   injective (@equiv (sig P) (sig_Setoid S)) (@equiv T S) (@proj1_sig T P).
 Proof using . intros * ?? H. cbn. apply H. Qed.
 
-Global Instance sigT_Setoid {T} (S : Setoid T) {P : T -> Type} : Setoid (sigT P).
+#[export]Instance sigT_Setoid {T} (S : Setoid T) {P : T -> Type} : Setoid (sigT P).
 simple refine {| equiv := fun x y => projT1 x == projT1 y |}; auto; [].
 Proof. split.
 + intro. reflexivity.
@@ -232,10 +232,10 @@ Proof. split.
 + intros ? ? ? ? ?. etransitivity; eauto.
 Defined.
 
-Global Instance sigT_EqDec {T} {S : Setoid T} (E : EqDec S) (P : T -> Type) : EqDec (@sigT_Setoid T S P).
+#[export]Instance sigT_EqDec {T} {S : Setoid T} (E : EqDec S) (P : T -> Type) : EqDec (@sigT_Setoid T S P).
 Proof. intros ? ?. simpl. apply equiv_dec. Defined.
 
-Global Instance projT1_compat {T} {S : Setoid T} (E : EqDec S) (P : T -> Type) :
+#[export]Instance projT1_compat {T} {S : Setoid T} (E : EqDec S) (P : T -> Type) :
   Proper (@equiv _ (sigT_Setoid S) ==> equiv) (@projT1 T P).
 Proof using . intros ?? H. apply H. Qed.
 
diff --git a/minipactole/minipactole.v b/minipactole/minipactole.v
index 409c74497aff01a964d1f8edd8ec0f6f24c1977c..aef316fbf954d6fa0d6932982b2b807184e030fd 100644
--- a/minipactole/minipactole.v
+++ b/minipactole/minipactole.v
@@ -121,8 +121,8 @@ Section Vig2Cols.
     intros.
     case x;case y.
     intros r r0 r1 r2. 
-    case (Rdec r1 r);intros;subst.
-    - case (Rdec r2 r0);intros;subst.
+    case (Req_dec_T r1 r);intros; subst.
+    - case (Req_dec_T r2 r0);intros;cbn [equiv] in *;subst.
       + left; reflexivity.
       + right.
         intro abs.