From 6fac6fe65dd8d3711310d76a6a06b96fb4af085b Mon Sep 17 00:00:00 2001
From: ndcroos <nick.decroos@gmail.com>
Date: Wed, 31 Jul 2024 15:47:51 +0200
Subject: [PATCH 1/5] removed 'easy' to 'done' replacements

---
 misc/stdpp_tactics.v | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 misc/stdpp_tactics.v

diff --git a/misc/stdpp_tactics.v b/misc/stdpp_tactics.v
new file mode 100644
index 0000000..6d095a5
--- /dev/null
+++ b/misc/stdpp_tactics.v
@@ -0,0 +1,36 @@
+From Coq Require Export RelationClasses Relation_Definitions Lia.
+
+Module FastDoneTactic.
+
+Lemma not_symmetry {A} `{R : relation A, !Symmetric R} x y : ~ R x y -> ~ R y x.
+Proof. intuition. Qed.
+
+Ltac fast_done :=
+  solve
+    [ eassumption
+    | symmetry; eassumption
+    | apply not_symmetry; eassumption
+    | reflexivity ].
+Tactic Notation "fast_by" tactic(tac) :=
+  tac; fast_done.
+
+End FastDoneTactic.
+
+Import FastDoneTactic.
+
+Ltac done :=
+  solve
+  [ repeat first
+    [ fast_done
+    | solve [trivial]
+    (* All the tactics below will introduce themselves anyway, or make no sense
+       for goals of product type. So this is a good place for us to do it. *)
+    | progress intros
+    | solve [symmetry; trivial]
+    | solve [apply not_symmetry; trivial]
+    | discriminate
+    | contradiction
+    | split
+    | match goal with H : ~ _ |- _ => case H; clear H; fast_done end ]
+  ].
+

From 128f03af2a6fb04f142206c834cc74945c3a8258 Mon Sep 17 00:00:00 2001
From: ndcroos <nick.decroos@gmail.com>
Date: Wed, 31 Jul 2024 16:18:03 +0200
Subject: [PATCH 2/5] Changes in implementations/option.v

---
 implementations/option.v | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/implementations/option.v b/implementations/option.v
index 789f7ba..de30325 100644
--- a/implementations/option.v
+++ b/implementations/option.v
@@ -1,5 +1,5 @@
 Require Import
-  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.jections MathClasses.theory.monads.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.jections MathClasses.theory.monads MathClasses.misc.stdpp_tactics.
 
 Inductive option_equiv A `{Equiv A} : Equiv (option A) :=
   | option_equiv_Some : Proper ((=) ==> (=)) Some
@@ -27,7 +27,7 @@ Section contents.
     intros x y z E. revert z. induction E.
      intros z E2. inversion_clear E2.
      apply option_equiv_Some. etransitivity; eassumption.
-    easy.
+    done.
   Qed.
 
   Global Instance: Setoid_Morphism Some.
@@ -59,7 +59,7 @@ Section contents.
        now apply E1.
       symmetry. now apply E1.
      now apply E1.
-    easy.
+    done.
   Qed.
 
   Global Program Instance option_dec `(A_dec : ∀ x y : A, Decision (x = y))
@@ -111,7 +111,7 @@ Instance option_bind_proper `{Setoid A} `{Setoid (option B)}: Proper (=) (option
 Proof.
   intros f₁ f₂ E1 x₁ x₂ [?|].
    unfold option_bind. simpl. now apply E1.
-  easy.
+  done.
 Qed.
 
 #[global]
@@ -122,8 +122,8 @@ Proof.
    now intros ? ? ? [?|].
   intros A ? B ? C ? ? f [???] g [???] [x|] [y|] E; try solve [inversion_clear E].
    setoid_inject. cut (g x = g y); [|now rewrite E].
-   case (g x), (g y); intros E2; inversion_clear E2. now f_equiv. easy.
-  easy.
+   case (g x), (g y); intros E2; inversion_clear E2. now f_equiv. done.
+  done.
 Qed.
 
 #[global]
@@ -140,7 +140,7 @@ Section map.
   Proof.
     pose proof (injective_mor f).
     repeat (split; try apply _).
-    intros [x|] [y|] E; try solve [inversion E | easy].
+    intros [x|] [y|] E; try solve [inversion E | done].
     apply sm_proper. apply (injective f). now apply (injective Some).
   Qed.
 End map.

From 6841062535da358a590bd62cdd954290204161ae Mon Sep 17 00:00:00 2001
From: ndcroos <nick.decroos@gmail.com>
Date: Wed, 31 Jul 2024 16:31:10 +0200
Subject: [PATCH 3/5] Changes in implementations/ZType_integers.v

---
 implementations/ZType_integers.v   | 8 ++++----
 implementations/stdlib_rationals.v | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/implementations/ZType_integers.v b/implementations/ZType_integers.v
index 65d98ed..dd296b0 100644
--- a/implementations/ZType_integers.v
+++ b/implementations/ZType_integers.v
@@ -1,6 +1,6 @@
 Require
   MathClasses.implementations.stdlib_binary_integers MathClasses.theory.integers MathClasses.orders.semirings.
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Bignums.SpecViaZ.ZSig Bignums.SpecViaZ.ZSigZAxioms Coq.NArith.NArith Coq.ZArith.ZArith
   MathClasses.implementations.nonneg_integers_naturals MathClasses.interfaces.orders
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.additional_operations.
@@ -52,7 +52,7 @@ Instance inject_ZType_Z: Cast t Z := to_Z.
 
 #[global]
 Instance: Proper ((=) ==> (=)) to_Z.
-Proof. intros x y E. easy. Qed.
+Proof. intros x y E. done. Qed.
 
 #[global]
 Instance: SemiRing_Morphism to_Z.
@@ -211,7 +211,7 @@ Proof.
    intros x1. apply axioms.pow_0_r.
   intros x [n ?].
   unfold_equiv. unfold "^", ZType_pow. simpl.
-  rewrite <-axioms.pow_succ_r; try easy.
+  rewrite <-axioms.pow_succ_r; try done.
   now rewrite ZType_succ_1_plus.
 Qed.
 
@@ -230,7 +230,7 @@ Proof.
   rewrite spec_mul, 2!spec_pow_N.
   rewrite rings.preserves_plus, Z.pow_add_r.
     now rewrite rings.preserves_1, Z.pow_1_r.
-   easy.
+   done.
   now apply Z_of_N_le_0.
 Qed.
 
diff --git a/implementations/stdlib_rationals.v b/implementations/stdlib_rationals.v
index 5334249..142e568 100644
--- a/implementations/stdlib_rationals.v
+++ b/implementations/stdlib_rationals.v
@@ -1,5 +1,5 @@
 Require
-  MathClasses.implementations.stdlib_binary_integers Coq.setoid_ring.Field Coq.QArith.Qfield MathClasses.theory.rationals.
+  MathClasses.implementations.stdlib_binary_integers Coq.setoid_ring.Field Coq.QArith.Qfield MathClasses.theory.rationals .
 Require Import
   Coq.ZArith.ZArith
   Coq.setoid_ring.Ring Coq.QArith.QArith_base Coq.QArith.Qabs Coq.QArith.Qpower

From 9da54fe59f14fc4d311bdf1623f8f65d26e4bba1 Mon Sep 17 00:00:00 2001
From: ndcroos <nick.decroos@gmail.com>
Date: Wed, 31 Jul 2024 20:29:44 +0200
Subject: [PATCH 4/5] Using not_symmetry that is already in MathClasses

---
 implementations/stdlib_rationals.v | 10 +++++-----
 misc/stdpp_tactics.v               |  4 +---
 2 files changed, 6 insertions(+), 8 deletions(-)

diff --git a/implementations/stdlib_rationals.v b/implementations/stdlib_rationals.v
index 142e568..8a5d097 100644
--- a/implementations/stdlib_rationals.v
+++ b/implementations/stdlib_rationals.v
@@ -1,6 +1,6 @@
 Require
   MathClasses.implementations.stdlib_binary_integers Coq.setoid_ring.Field Coq.QArith.Qfield MathClasses.theory.rationals .
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Coq.ZArith.ZArith
   Coq.setoid_ring.Ring Coq.QArith.QArith_base Coq.QArith.Qabs Coq.QArith.Qpower
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.rationals
@@ -61,7 +61,7 @@ Program Instance Q_to_fracZ: Cast Q (Frac Z) := λ x, frac (Qnum x) (Zpos (Qden
 
 #[global]
 Instance: Proper ((=) ==> (=)) Q_to_fracZ.
-Proof. intros ? ? E. easy. Qed.
+Proof. intros ? ? E. done. Qed.
 
 #[global]
 Instance: SemiRing_Morphism Q_to_fracZ.
@@ -69,7 +69,7 @@ Proof. repeat (split; try apply _). Qed.
 
 #[global]
 Instance: Injective Q_to_fracZ.
-Proof. split; try apply _. intros ? ? E. easy. Qed.
+Proof. split; try apply _. intros ? ? E. done. Qed.
 
 #[global]
 Instance: RationalsToFrac Q := rationals.alt_to_frac Q_to_fracZ.
@@ -92,7 +92,7 @@ Proof.
    exact Qle_antisym.
   apply (rings.from_ring_order (Rle:=Q_le)).
    repeat (split; try apply _).
-   intros. apply Qplus_le_compat. now apply Qle_refl. easy.
+   intros. apply Qplus_le_compat. now apply Qle_refl. done.
   intros. now apply Qmult_le_0_compat.
 Qed.
 
@@ -110,7 +110,7 @@ Proof.
   rapply (semirings.dec_full_pseudo_srorder (R:=Q)).
   split.
    intro. split. now apply Zorder.Zlt_le_weak. now apply Zorder.Zlt_not_eq.
-  intros [E1 E2]. destruct (Zorder.Zle_lt_or_eq _ _ E1). easy. now destruct E2.
+  intros [E1 E2]. destruct (Zorder.Zle_lt_or_eq _ _ E1). done. now destruct E2.
 Qed.
 
 #[global]
diff --git a/misc/stdpp_tactics.v b/misc/stdpp_tactics.v
index 6d095a5..b853f1d 100644
--- a/misc/stdpp_tactics.v
+++ b/misc/stdpp_tactics.v
@@ -1,10 +1,8 @@
+Require Import MathClasses.misc.util.
 From Coq Require Export RelationClasses Relation_Definitions Lia.
 
 Module FastDoneTactic.
 
-Lemma not_symmetry {A} `{R : relation A, !Symmetric R} x y : ~ R x y -> ~ R y x.
-Proof. intuition. Qed.
-
 Ltac fast_done :=
   solve
     [ eassumption

From 3366a1232565e4b70aab0958243ea2fa19f3cf35 Mon Sep 17 00:00:00 2001
From: ndcroos <nick.decroos@gmail.com>
Date: Wed, 31 Jul 2024 22:30:23 +0200
Subject: [PATCH 5/5] Added changes from 'easy' to 'done'

---
 implementations/dyadics.v                |   4 +-
 implementations/list.v                   |  10 +-
 implementations/list_finite_set.v        |  16 +--
 implementations/option.v                 |   2 +-
 implementations/polynomials.v            |  45 ++++----
 implementations/stdlib_binary_integers.v |   4 +-
 orders/dec_fields.v                      |   4 +-
 orders/lattices.v                        |  18 +--
 orders/maps.v                            |  10 +-
 orders/minmax.v                          |   6 +-
 orders/nat_int.v                         |   6 +-
 orders/naturals.v                        |   4 +-
 orders/semirings.v                       |  32 +++---
 theory/abs.v                             |   6 +-
 theory/cut_minus.v                       |  90 +++++++--------
 theory/dec_fields.v                      |   6 +-
 theory/groups.v                          |   4 +-
 theory/int_abs.v                         |   4 +-
 theory/int_pow.v                         |  14 +--
 theory/int_to_nat.v                      |  14 +--
 theory/jections.v                        |   4 +-
 theory/monads.v                          |   4 +-
 theory/nat_pow.v                         |  14 +--
 theory/naturals.v                        |   4 +-
 theory/streams.v                         |   8 +-
 theory/strong_setoids.v                  | 136 +++++++++++------------
 varieties/monoids.v                      |   4 +-
 varieties/semigroups.v                   |   4 +-
 28 files changed, 239 insertions(+), 238 deletions(-)

diff --git a/implementations/dyadics.v b/implementations/dyadics.v
index 1ec24d2..aae31ef 100644
--- a/implementations/dyadics.v
+++ b/implementations/dyadics.v
@@ -3,8 +3,8 @@
    for some [Integers] implementation [Z]. These numbers form a ring and can be
    embedded into any [Rationals] implementation [Q].
 *)
-Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra
+Require Import 
+  Coq.setoid_ring.Ring  MathClasses.interfaces.abstract_algebra
   MathClasses.interfaces.integers MathClasses.interfaces.naturals MathClasses.interfaces.rationals
   MathClasses.interfaces.additional_operations MathClasses.interfaces.orders
   MathClasses.orders.minmax MathClasses.orders.integers MathClasses.orders.rationals
diff --git a/implementations/list.v b/implementations/list.v
index a8dadc7..f25e278 100644
--- a/implementations/list.v
+++ b/implementations/list.v
@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads.
 Import ListNotations.
 
@@ -29,7 +29,7 @@ Section equivlistA_misc.
   Proof. intros E. now eapply InA_nil, E, InA_cons_hd. Qed.
 
   Lemma equivlistA_nil_eq l : equivlistA eqA l [] → l ≡ [].
-  Proof. induction l. easy. intros E. edestruct equivlistA_cons_nil; eauto. Qed.
+  Proof. induction l. done. intros E. edestruct equivlistA_cons_nil; eauto. Qed.
 
   Lemma InA_double_head z x l : InA eqA z (x :: x :: l) ↔ InA eqA z (x :: l).
   Proof. split; intros E1; auto. inversion_clear E1; auto. Qed.
@@ -91,14 +91,14 @@ Section equivlistA_misc.
 
   Lemma PermutationA_app_head l₁ l₂ k :
     PermutationA l₁ l₂ → PermutationA (k ++ l₁) (k ++ l₂).
-  Proof. intros. induction k. easy. apply permA_skip; intuition. Qed.
+  Proof. intros. induction k. done. apply permA_skip; intuition. Qed.
 
   Global Instance PermutationA_app :
     Proper (PermutationA ==> PermutationA ==> PermutationA) (@app A).
   Proof.
     intros  l₁ l₂ Pl k₁ k₂ Pk.
     induction Pl.
-       easy.
+       done.
       now apply permA_skip.
      etransitivity.
       rewrite <-!app_comm_cons. now apply permA_swap.
@@ -113,7 +113,7 @@ Section equivlistA_misc.
 
   Lemma PermutationA_cons_append l x :
     PermutationA (x :: l) (l ++ x :: nil).
-  Proof. induction l. easy. simpl. rewrite <-IHl. intuition. Qed.
+  Proof. induction l. done. simpl. rewrite <-IHl. intuition. Qed.
 
   Lemma PermutationA_app_comm l₁ l₂ :
     PermutationA (l₁ ++ l₂) (l₂ ++ l₁).
diff --git a/implementations/list_finite_set.v b/implementations/list_finite_set.v
index 91f2534..7ffc84d 100644
--- a/implementations/list_finite_set.v
+++ b/implementations/list_finite_set.v
@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Coq.Lists.List Coq.Lists.SetoidList MathClasses.implementations.list
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.finite_sets MathClasses.interfaces.orders
   MathClasses.theory.lattices MathClasses.orders.lattices.
@@ -48,7 +48,7 @@ Proof. firstorder. Qed.
 Global Instance: Proper ((=) ==> (=) ==> iff) listset_in.
 Proof.
   intros x y E1 l k E2.
-  transitivity (listset_in x k). easy.
+  transitivity (listset_in x k). done.
   unfold listset_in. now rewrite E1.
 Qed.
 
@@ -108,7 +108,7 @@ Lemma listset_to_list_preserves_join l k :
 Proof.
   destruct l as [l Pl], k as [k Pk].
   unfold join, listset_join, listset_join_raw. simpl. clear Pk Pl.
-  induction l; simpl; intros; [easy|].
+  induction l; simpl; intros; [done|].
   now rewrite <-IHl, listset_add_raw_cons.
 Qed.
 
@@ -161,7 +161,7 @@ Section listset_extend.
   Proof.
     induction 1; simpl.
        reflexivity.
-      apply sg_op_proper. now apply sm_proper. easy.
+      apply sg_op_proper. now apply sm_proper. done.
      now rewrite !associativity, (commutativity (f _)).
     etransitivity; eassumption.
   Qed.
@@ -180,7 +180,7 @@ Section listset_extend.
     fset_extend f ({{x}} ⊔ l) = f x ⊔ fset_extend f l.
   Proof.
     destruct l as [l Pl]. unfold fset_extend, list_extend. simpl. clear Pl.
-    induction l; simpl; [easy|].
+    induction l; simpl; [done|].
     case (decide_rel _); intros E.
      now rewrite E, associativity, (idempotency (&) _).
     now rewrite IHl, 2!associativity, (commutativity (f _)).
@@ -215,7 +215,7 @@ Proof.
     solve_proper.
    now rewrite preserves_bottom.
   intros x l E2 E3. rewrite list_extend_add, preserves_join, E3.
-  apply sg_op_proper; [|easy]. symmetry. now apply E1.
+  apply sg_op_proper; [|done]. symmetry. now apply E1.
 Qed.
 
 Instance: FSetContainsSpec A.
@@ -251,7 +251,7 @@ Proof.
     intros E1; inversion E1.
    case (decide_rel); intros ? E1; intuition.
    inversion_clear E1 as [?? E2|]; auto. now rewrite E2.
-  intros [E1 E2]. induction l; simpl; [easy|].
+  intros [E1 E2]. induction l; simpl; [done|].
   case (decide_rel); intros E3.
    inversion_clear E1; intuition.
   inversion_clear E1 as [?? E4|]; intuition.
@@ -292,7 +292,7 @@ Proof.
    case (decide_rel); intros ? E1.
     intuition.
    inversion_clear E1 as [?? E2|]; auto. now rewrite E2.
-  intros [E1 E2]. induction l; simpl; [easy|].
+  intros [E1 E2]. induction l; simpl; [done|].
   case (decide_rel); intros E3.
    inversion_clear E1 as [?? E4|]; intuition.
    destruct E2. now rewrite E4.
diff --git a/implementations/option.v b/implementations/option.v
index de30325..2c47eec 100644
--- a/implementations/option.v
+++ b/implementations/option.v
@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.jections MathClasses.theory.monads MathClasses.misc.stdpp_tactics.
 
 Inductive option_equiv A `{Equiv A} : Equiv (option A) :=
diff --git a/implementations/polynomials.v b/implementations/polynomials.v
index 494698f..3114f10 100644
--- a/implementations/polynomials.v
+++ b/implementations/polynomials.v
@@ -1,4 +1,5 @@
-Require Import
+Require Import 
+  MathClasses.misc.stdpp_tactics
   Coq.Lists.List
   MathClasses.interfaces.abstract_algebra
   MathClasses.interfaces.vectorspace
@@ -63,7 +64,7 @@ Section contents.
 
   Lemma poly_eq_cons :
     ∀ (a b : R) (p q : poly), (a = b /\ poly_eq p q) <-> poly_eq (a :: p) (b :: q).
-  Proof. easy. Qed.
+  Proof. done. Qed.
 
   Lemma poly_eq_ind (P: poly → poly → Prop)
         (case_0: ∀ p p', poly_eq_zero p → poly_eq_zero p' → P p p')
@@ -134,7 +135,7 @@ Section contents.
   Proof.
     intro eqp; revert q.
     induction eqp as [|x p eqx eqp IH] using poly_eq_zero_ind.
-    { easy. }
+    { done. }
     intros [|y q].
     { cbn -[poly_eq_zero].
       rewrite poly_eq_zero_cons; auto. }
@@ -143,7 +144,7 @@ Section contents.
   Qed.
 
   Instance plus_commutative: Commutative (+).
-  Proof with (try easy); cbn.
+  Proof with (try done); cbn.
     intro.
     induction x as [|x p IH]; intros [|y q]...
     split; auto; ring.
@@ -179,7 +180,7 @@ Section contents.
   Qed.
 
   Instance plus_associative: Associative (+).
-  Proof with try easy.
+  Proof with try done.
     do 2 red; induction x as [|x p IH]...
     intros [|y q]...
     intros [|z r]...
@@ -200,7 +201,7 @@ Section contents.
   Lemma poly_negate_zero p: poly_eq_zero p ↔ poly_eq_zero (-p).
   Proof.
     induction p as [|x p IH].
-    { easy. }
+    { done. }
     cbn.
     rewrite !poly_eq_zero_cons, IH.
     enough (x = 0 ↔ -x = 0) by tauto.
@@ -219,7 +220,7 @@ Section contents.
   Proof.
     intro; rewrite poly_eq_p_zero.
     induction x as [|x p IH]; cbn.
-    { easy. }
+    { done. }
     rewrite poly_eq_zero_cons; split; auto.
     ring.
   Qed.
@@ -239,7 +240,7 @@ Section contents.
   Lemma poly_scalar_mult_0_r q c: poly_eq_zero q → poly_eq_zero (c · q).
   Proof.
     induction q as [|x q IH].
-    { easy. }
+    { done. }
     cbn.
     rewrite !poly_eq_zero_cons.
     intros [-> ?]; split; auto.
@@ -257,36 +258,36 @@ Section contents.
   Qed.
 
   Lemma poly_scalar_mult_1_r x: x · 1 = [x].
-  Proof. cbn; split; [ring|easy]. Qed.
+  Proof. cbn; split; [ring|done]. Qed.
   Instance poly_scalar_mult_1_l: LeftIdentity (·) 1.
   Proof.
-    red; induction y as [|y p IH]; [easy|cbn].
+    red; induction y as [|y p IH]; [done|cbn].
     split; auto; ring.
   Qed.
 
   Instance poly_scalar_mult_dist_l: LeftHeteroDistribute (·) (+) (+).
   Proof.
     intros a p.
-    induction p as [|x p IH]; intros [|y q]; [easy..|cbn].
+    induction p as [|x p IH]; intros [|y q]; [done..|cbn].
     split; auto; ring.
   Qed.
   Instance poly_scalar_mult_dist_r: RightHeteroDistribute (·) (+) (+).
   Proof.
     intros a b x.
-    induction x as [|x p IH]; [easy|cbn].
+    induction x as [|x p IH]; [done|cbn].
     split; auto; ring.
   Qed.
   Instance poly_scalar_mult_assoc: HeteroAssociative (·) (·) (·) (.*.).
   Proof.
     intros a b x.
-    induction x as [|p x IH]; [easy|cbn].
+    induction x as [|p x IH]; [done|cbn].
     split; auto; ring.
   Qed.
 
   Lemma poly_scalar_mult_0_l q c: c = 0 → poly_eq_zero (c · q).
   Proof.
     intros ->.
-    induction q as [|x q IH]; [easy|cbn].
+    induction q as [|x q IH]; [done|cbn].
     rewrite poly_eq_zero_cons; split; auto.
     ring.
   Qed.
@@ -299,7 +300,7 @@ Section contents.
 
   Lemma poly_mult_0_l p q: poly_eq_zero p → poly_eq_zero (p * q).
   Proof.
-    induction 1 using poly_eq_zero_ind; [easy|cbn].
+    induction 1 using poly_eq_zero_ind; [done|cbn].
     apply poly_eq_zero_plus.
     - now apply poly_scalar_mult_0_l.
     - rewrite poly_eq_zero_cons; auto.
@@ -307,7 +308,7 @@ Section contents.
 
   Lemma poly_mult_0_r p q: poly_eq_zero q → poly_eq_zero (p * q).
   Proof.
-    induction p as [|x p IH]; [easy|cbn].
+    induction p as [|x p IH]; [done|cbn].
     intro eq0.
     apply poly_eq_zero_plus.
     - now apply poly_scalar_mult_0_r.
@@ -330,12 +331,12 @@ Section contents.
   Instance poly_mult_left_distr: LeftDistribute (.*.) (+).
   Proof.
     intros p q r.
-    induction p as [|x p IH]; [easy|cbn].
+    induction p as [|x p IH]; [done|cbn].
     rewrite (distribute_l x q r ).
-    rewrite <- !associativity; apply poly_plus_proper; [easy|].
+    rewrite <- !associativity; apply poly_plus_proper; [done|].
     rewrite associativity, (commutativity (0::p*q)), <- associativity.
-    apply poly_plus_proper; [easy|].
-    cbn; split; [ring|easy].
+    apply poly_plus_proper; [done|].
+    cbn; split; [ring|done].
   Qed.
 
   Lemma poly_mult_cons_r p q x: p * (x::q) = x · p + (0 :: p * q).
@@ -343,7 +344,7 @@ Section contents.
     induction p as [|y p IH]; cbn; auto.
     split; auto.
     rewrite IH, !associativity, (commutativity (y · q)).
-    split; try easy.
+    split; try done.
     ring.
   Qed.
 
@@ -383,7 +384,7 @@ Section contents.
   Qed.
 
   Instance poly_mult_assoc: Associative (.*.).
-  Proof with (try easy); cbn.
+  Proof with (try done); cbn.
     intros x.
     induction x as [|x p IH]...
     intros q r; cbn.
diff --git a/implementations/stdlib_binary_integers.v b/implementations/stdlib_binary_integers.v
index 9dd7150..ad3da76 100644
--- a/implementations/stdlib_binary_integers.v
+++ b/implementations/stdlib_binary_integers.v
@@ -1,6 +1,6 @@
 Require
   MathClasses.interfaces.naturals MathClasses.theory.naturals MathClasses.implementations.peano_naturals MathClasses.theory.integers.
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Coq.ZArith.BinInt Coq.setoid_ring.Ring Coq.Arith.Arith Coq.NArith.NArith Coq.ZArith.ZArith Coq.Numbers.Integer.Binary.ZBinary
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers
   MathClasses.implementations.natpair_integers MathClasses.implementations.stdlib_binary_naturals
@@ -152,7 +152,7 @@ Proof.
   rapply semirings.dec_full_pseudo_srorder.
   split.
    intro. split. now apply Zorder.Zlt_le_weak. now apply Zorder.Zlt_not_eq.
-  intros [E1 E2]. destruct (Zorder.Zle_lt_or_eq _ _ E1). easy. now destruct E2.
+  intros [E1 E2]. destruct (Zorder.Zle_lt_or_eq _ _ E1). done. now destruct E2.
 Qed.
 
 (* * Embedding of the Peano naturals into [Z] *)
diff --git a/orders/dec_fields.v b/orders/dec_fields.v
index b28c3ab..c925547 100644
--- a/orders/dec_fields.v
+++ b/orders/dec_fields.v
@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Coq.Relations.Relation_Definitions Coq.setoid_ring.Ring
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.theory.dec_fields.
 Require Export
@@ -22,7 +22,7 @@ Proof.
   destruct (decide (x = 0)) as [E2 | E2].
    now rewrite E2, dec_recip_0.
   apply lt_le. apply pos_dec_recip_compat.
-  apply lt_iff_le_ne. split. easy. now apply not_symmetry.
+  apply lt_iff_le_ne. split. done. now apply not_symmetry.
 Qed.
 
 Lemma neg_dec_recip_compat x : x < 0 → /x < 0.
diff --git a/orders/lattices.v b/orders/lattices.v
index 8ac47e6..b3a1843 100644
--- a/orders/lattices.v
+++ b/orders/lattices.v
@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.maps MathClasses.theory.lattices.
 
 (*
@@ -49,7 +49,7 @@ Section join_semilattice_order.
   Qed.
 
   Lemma join_le_compat_r x y z : z ≤ x → z ≤ x ⊔ y.
-  Proof. intros E. transitivity x. easy. apply join_ub_l. Qed.
+  Proof. intros E. transitivity x. done. apply join_ub_l. Qed.
   Lemma join_le_compat_l x y z : z ≤ y → z ≤ x ⊔ y.
   Proof. intros E. rewrite commutativity. now apply join_le_compat_r. Qed.
 
@@ -133,7 +133,7 @@ Section meet_semilattice_order.
   Qed.
 
   Lemma meet_le_compat_r x y z : x ≤ z → x ⊓ y ≤ z.
-  Proof. intros E. transitivity x. apply meet_lb_l. easy. Qed.
+  Proof. intros E. transitivity x. apply meet_lb_l. done. Qed.
   Lemma meet_le_compat_l x y z : y ≤ z → x ⊓ y ≤ z.
   Proof. intros E. rewrite commutativity. now apply meet_le_compat_r. Qed.
 
@@ -174,13 +174,13 @@ Section lattice_order.
   Proof.
     intros x y. apply (antisymmetry (≤)).
      now apply meet_lb_l.
-    apply meet_le. easy. now apply join_ub_l.
+    apply meet_le. done. now apply join_ub_l.
   Qed.
 
   Instance: Absorption (⊔) (⊓).
   Proof.
     intros x y. apply (antisymmetry (≤)).
-     apply join_le. easy. now apply meet_lb_l.
+     apply join_le. done. now apply meet_lb_l.
     now apply join_ub_l.
   Qed.
 
@@ -293,8 +293,8 @@ Section order_preserving_join_sl_mor.
   Proof.
     repeat (split; try apply _).
     intros x y. case (total (≤) x y); intros E.
-     rewrite 2!join_r; try easy. now apply (order_preserving _).
-    rewrite 2!join_l; try easy. now apply (order_preserving _).
+     rewrite 2!join_r; try done. now apply (order_preserving _).
+    rewrite 2!join_l; try done. now apply (order_preserving _).
   Qed.
 End order_preserving_join_sl_mor.
 
@@ -309,7 +309,7 @@ Section order_preserving_meet_sl_mor.
   Proof.
     repeat (split; try apply _).
     intros x y. case (total (≤) x y); intros E.
-     rewrite 2!meet_l; try easy. now apply (order_preserving _).
-    rewrite 2!meet_r; try easy. now apply (order_preserving _).
+     rewrite 2!meet_l; try done. now apply (order_preserving _).
+    rewrite 2!meet_r; try done. now apply (order_preserving _).
   Qed.
 End order_preserving_meet_sl_mor.
diff --git a/orders/maps.v b/orders/maps.v
index 5b70258..d9efa93 100644
--- a/orders/maps.v
+++ b/orders/maps.v
@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.orders MathClasses.theory.setoids MathClasses.theory.strong_setoids.
 
 Local Existing Instance order_morphism_po_a.
@@ -247,11 +247,11 @@ Proof. pose proof po_setoid. repeat (split; try apply _). Qed.
 
 #[global]
 Instance id_order_preserving `{PartialOrder A} : OrderPreserving (@id A).
-Proof. split; try apply _. easy. Qed.
+Proof. split; try apply _. done. Qed.
 
 #[global]
 Instance id_order_reflecting `{PartialOrder A} : OrderReflecting (@id A).
-Proof. split; try apply _. easy. Qed.
+Proof. split; try apply _. done. Qed.
 
 Section composition.
   Context `{Equiv A} `{Equiv B} `{Equiv C}
@@ -297,7 +297,7 @@ Section propers.
   Proof.
     assert (∀ (f g : A → B), g = f → Order_Morphism f → Order_Morphism g) as P.
      intros f g E [[? ? ?] ?].
-     split; auto. apply morphism_proper with f. easy. split; easy.
+     split; auto. apply morphism_proper with f. done. split; done.
     firstorder.
   Qed.
 
@@ -329,7 +329,7 @@ Section propers.
       eapply order_preserving_proper; eauto. now apply _.
      eapply order_reflecting_proper; eauto. now apply _.
     intros f g ?; split; intro E.
-     apply P with f. destruct E as [[[[? ?]]]]. now symmetry. easy.
+     apply P with f. destruct E as [[[[? ?]]]]. now symmetry. done.
     now apply P with g.
   Qed.
 End propers.
diff --git a/orders/minmax.v b/orders/minmax.v
index 01df5c1..1ec7710 100644
--- a/orders/minmax.v
+++ b/orders/minmax.v
@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.orders
   MathClasses.orders.lattices MathClasses.theory.setoids.
 
@@ -24,14 +24,14 @@ Section contents.
   Global Instance: LatticeOrder (≤).
   Proof.
     repeat (split; try apply _); unfold join, meet, max, min, sort;
-     intros; case (decide_rel _); try easy; now apply le_flip.
+     intros; case (decide_rel _); try done; now apply le_flip.
   Qed.
 
   Instance: LeftDistribute max min.
   Proof.
     intros x y z. unfold min, max, sort.
     repeat case (decide_rel _); simpl; try solve [intuition].
-     intros. apply (antisymmetry (≤)); [|easy]. now transitivity y; apply le_flip.
+     intros. apply (antisymmetry (≤)); [|done]. now transitivity y; apply le_flip.
     intros. now apply (antisymmetry (≤)).
   Qed.
 
diff --git a/orders/nat_int.v b/orders/nat_int.v
index 22215eb..90bcc03 100644
--- a/orders/nat_int.v
+++ b/orders/nat_int.v
@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders
   MathClasses.theory.naturals MathClasses.theory.rings MathClasses.implementations.peano_naturals.
 Require Export
@@ -21,7 +21,7 @@ Proof.
     solve_proper.
    intros. now rewrite preserves_0.
   intros n E. rewrite preserves_plus, preserves_1.
-  apply nonneg_plus_compat. solve_propholds. easy.
+  apply nonneg_plus_compat. solve_propholds. done.
 Qed.
 
 Section nat_int_order.
@@ -96,7 +96,7 @@ Lemma pos_ge_1 x : 0 < x ↔ 1 ≤ x.
 Proof.
   split; intros E.
    rewrite <-(plus_0_l 1). now apply lt_iff_plus_1_le.
-  apply lt_le_trans with 1; [solve_propholds | easy].
+  apply lt_le_trans with 1; [solve_propholds | done].
 Qed.
 
 Lemma le_iff_lt_plus_1 x y : x ≤ y ↔ x < y + 1.
diff --git a/orders/naturals.v b/orders/naturals.v
index be6ba7f..3f30a02 100644
--- a/orders/naturals.v
+++ b/orders/naturals.v
@@ -1,6 +1,6 @@
 Require
   MathClasses.theory.naturals.
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.orders.rings.
 Require Export
   MathClasses.orders.nat_int.
@@ -16,7 +16,7 @@ Proof.
   split; intros E.
    destruct (decompose_le E) as [z [Ez1 Ez2]]. now exists z.
   destruct E as [z Ez].
-  apply compose_le with z; [solve_propholds | easy].
+  apply compose_le with z; [solve_propholds | done].
 Qed.
 
 Lemma nat_not_neg x : ¬x < 0.
diff --git a/orders/semirings.v b/orders/semirings.v
index a1ce9ed..19b433d 100644
--- a/orders/semirings.v
+++ b/orders/semirings.v
@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings.
 Require Export
   MathClasses.orders.orders MathClasses.orders.maps.
@@ -61,7 +61,7 @@ Section semiring_order.
   Proof.
     intros E.
     destruct (srorder_partial_minus x y E) as [z Ez].
-    exists z. split; [| easy].
+    exists z. split; [| done].
     apply (order_reflecting (x+)).
     now rewrite plus_0_r, <-Ez.
   Qed.
@@ -93,14 +93,14 @@ Section semiring_order.
     intros Ex₁ Ey₁ E1 E2.
     transitivity (y₁ * x₂).
      now apply (order_preserving_flip_nonneg (.*.) x₂).
-    apply (order_preserving_nonneg (.*.) y₁); [| easy].
+    apply (order_preserving_nonneg (.*.) y₁); [| done].
     now transitivity x₁.
   Qed.
 
   Lemma ge_1_mult_le_compat_r x y z : 1 ≤ z → 0 ≤ y → x ≤ y → x ≤ y * z.
   Proof.
     intros.
-    transitivity y; [easy |].
+    transitivity y; [done |].
     rewrite <-(mult_1_r y) at 1.
     now apply (order_preserving_nonneg (.*.) y).
   Qed.
@@ -200,7 +200,7 @@ Section strict_semiring_order.
   Proof.
     intros E.
     destruct (strict_srorder_partial_minus x y E) as [z Ez].
-    exists z. split; [| easy].
+    exists z. split; [| done].
     apply (strictly_order_reflecting (x+)).
     now rewrite <-Ez, rings.plus_0_r.
   Qed.
@@ -223,14 +223,14 @@ Section strict_semiring_order.
     intros Ex₁ Ey₁ E1 E2.
     transitivity (y₁ * x₂).
      now apply (strictly_order_preserving_flip_pos (.*.) x₂).
-    apply (strictly_order_preserving_pos (.*.) y₁); [| easy ].
+    apply (strictly_order_preserving_pos (.*.) y₁); [| done ].
     now transitivity x₁.
   Qed.
 
   Lemma gt_1_mult_lt_compat_r x y z : 1 < z → 0 < y → x < y → x < y * z.
   Proof.
     intros.
-    transitivity y; [ easy |].
+    transitivity y; [ done |].
     rewrite <-(mult_1_r y) at 1.
     now apply (strictly_order_preserving_pos (.*.) y).
   Qed.
@@ -320,10 +320,10 @@ Section pseudo_semiring_order.
     rewrite apart_iff_total_lt in Ex, Ey.
     destruct Ex as [Ex|Ex], Ey as [Ey|Ey]; try tauto.
      destruct (irreflexivity (<) 0).
-     transitivity (x * y); [| easy].
+     transitivity (x * y); [| done].
      now apply pos_mult_compat.
     destruct (irreflexivity (<) 0).
-    transitivity (x * y); [| easy].
+    transitivity (x * y); [| done].
     now apply neg_mult.
   Qed.
 
@@ -339,10 +339,10 @@ Section pseudo_semiring_order.
     rewrite apart_iff_total_lt in Ex, Ey.
     destruct Ex as [Ex|Ex], Ey as [Ey|Ey]; try tauto.
      destruct (irreflexivity (<) 0).
-     transitivity (x * y); [easy |].
+     transitivity (x * y); [done |].
      now apply pos_neg_mult.
     destruct (irreflexivity (<) 0).
-    transitivity (x * y); [easy |].
+    transitivity (x * y); [done |].
     now apply neg_pos_mult.
   Qed.
 
@@ -398,7 +398,7 @@ Section pseudo_semiring_order.
   Proof. intros. apply (strictly_order_reflecting (.* y)). now rewrite rings.mult_0_l. Qed.
 
   Lemma pos_mult_rev_r x y : 0 < x * y → 0 < x → 0 < y.
-  Proof. intros. apply pos_mult_rev_l with x. now rewrite commutativity. easy. Qed.
+  Proof. intros. apply pos_mult_rev_l with x. now rewrite commutativity. done. Qed.
 
   Context `{PropHolds (1 ≶ 0)}.
 
@@ -509,7 +509,7 @@ Section full_pseudo_semiring_order.
   Proof.
     apply not_lt_le_flip. intros E.
     destruct (lt_antisym (x * x) 0).
-    split; [easy |].
+    split; [done |].
     apply square_pos.
     apply (strong_extensionality (x *.)).
     rewrite mult_0_r.
@@ -520,7 +520,7 @@ Section full_pseudo_semiring_order.
   Proof. intros. apply (order_reflecting (.* y)). now rewrite rings.mult_0_l. Qed.
 
   Lemma nonneg_mult_rev_r x y : 0 ≤ x * y → 0 < x → 0 ≤ y.
-  Proof. intros. apply nonneg_mult_rev_l with x. now rewrite commutativity. easy. Qed.
+  Proof. intros. apply nonneg_mult_rev_l with x. now rewrite commutativity. done. Qed.
 
   Instance le_0_1 : PropHolds (0 ≤ 1).
   Proof. red. setoid_replace 1 with (1 * 1) by ring. now apply square_nonneg. Qed.
@@ -556,14 +556,14 @@ Section full_pseudo_semiring_order.
   Proof.
     intros.
     apply ge_1_mult_le_compat_r; trivial.
-    transitivity 1. now apply le_0_1. easy.
+    transitivity 1. now apply le_0_1. done.
   Qed.
 
   Lemma gt_1_ge_1_mult_compat x y : 1 < x → 1 ≤ y → 1 < x * y.
   Proof.
     intros.
     apply lt_le_trans with x; trivial.
-    apply ge_1_mult_le_compat_r; try easy.
+    apply ge_1_mult_le_compat_r; try done.
     transitivity 1. now apply le_0_1. now apply lt_le.
   Qed.
 
diff --git a/theory/abs.v b/theory/abs.v
index 48e08cf..561d344 100644
--- a/theory/abs.v
+++ b/theory/abs.v
@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.rings.
 
 Section contents.
@@ -31,7 +31,7 @@ Lemma abs_nonneg_plus (x y : R) :
   0 ≤ x → 0 ≤ y → abs (x + y) = abs x + abs y.
 Proof.
   intros Ex Ey.
-  rewrite ?abs_nonneg; try easy.
+  rewrite ?abs_nonneg; try done.
   now apply nonneg_plus_compat.
 Qed.
 
@@ -99,7 +99,7 @@ Section order_preserving.
   Lemma preserves_abs x : f (abs x) = abs (f x).
   Proof.
     destruct (total (≤) 0 x).
-     rewrite ?abs_nonneg; try easy.
+     rewrite ?abs_nonneg; try done.
      now apply semirings.preserves_nonneg.
     rewrite ?abs_nonpos; try easy.
      apply rings.preserves_negate.
diff --git a/theory/cut_minus.v b/theory/cut_minus.v
index 32e5233..2ab0664 100644
--- a/theory/cut_minus.v
+++ b/theory/cut_minus.v
@@ -1,6 +1,6 @@
 Require
   MathClasses.orders.semirings.
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations
   MathClasses.interfaces.orders MathClasses.orders.minmax.
 
@@ -19,9 +19,9 @@ Section cut_minus_properties.
   Proof.
     intros x₁ x₂ E y₁ y₂ F.
     destruct (total (≤) x₂ y₂).
-     rewrite cut_minus_0, cut_minus_0; try easy. now rewrite E, F.
+     rewrite cut_minus_0, cut_minus_0; try done. now rewrite E, F.
     apply (right_cancellation (+) y₂).
-    rewrite cut_minus_le by easy.
+    rewrite cut_minus_le by done.
     rewrite <-E, <-F. apply cut_minus_le. now rewrite E, F.
   Qed.
 
@@ -65,7 +65,7 @@ Section cut_minus_properties.
   Lemma cut_minus_le_trans x y z : y ≤ x → z ≤ y → (x ∸ y) + (y ∸ z) = x ∸ z.
   Proof.
     intros. apply (right_cancellation (+) z).
-    rewrite <-associativity, !cut_minus_le; try easy.
+    rewrite <-associativity, !cut_minus_le; try done.
     now transitivity y.
   Qed.
   Hint Resolve cut_minus_le_trans.
@@ -90,7 +90,7 @@ Section cut_minus_properties.
       ring.
      now apply (maps.order_preserving_nonneg (.*.) x).
     apply (right_cancellation (+) (x * z)).
-    rewrite <-distribute_l, !cut_minus_le; try easy.
+    rewrite <-distribute_l, !cut_minus_le; try done.
     now apply (maps.order_preserving_nonneg (.*.) x).
   Qed.
 
@@ -106,7 +106,7 @@ Section cut_minus_properties.
      rewrite !cut_minus_0; intuition.
     apply (right_cancellation (+) (x + z)).
     transitivity ((y ∸ z + z) + x); try ring.
-    rewrite !cut_minus_le; try easy; try ring.
+    rewrite !cut_minus_le; try done; try ring.
     now apply (order_preserving (x +)).
   Qed.
 
@@ -117,8 +117,8 @@ Section cut_minus_properties.
   Lemma cut_minus_plus_r x y z : 0 ≤ z → x ∸ (y + z) = (x ∸ y) ∸ z.
   Proof.
     intros E. case (total (≤) x y); intros Exy.
-     rewrite (cut_minus_0 x y) by easy.
-     rewrite cut_minus_0_l, cut_minus_0; try easy.
+     rewrite (cut_minus_0 x y) by done.
+     rewrite cut_minus_0_l, cut_minus_0; try done.
      now apply semirings.plus_le_compat_r.
     rewrite (cut_minus_plus_rev_r y (x ∸ y) z).
     now rewrite cut_minus_le, commutativity.
@@ -130,28 +130,28 @@ Section cut_minus_properties.
   Lemma cut_minus_plus_toggle1 x y z : x ≤ y → z ≤ y → (y ∸ x) + (x ∸ z) = (y ∸ z) + (z ∸ x).
   Proof.
     intros. destruct (total (≤) x z).
-     rewrite (cut_minus_0 x z), cut_minus_le_trans by easy. ring.
-    rewrite (cut_minus_0 z x), cut_minus_le_trans by easy. ring.
+     rewrite (cut_minus_0 x z), cut_minus_le_trans by done. ring.
+    rewrite (cut_minus_0 z x), cut_minus_le_trans by done. ring.
   Qed.
 
   Lemma cut_minus_plus_toggle2 x y z : y ≤ x → y ≤ z →  (x ∸ z) + (z ∸ y) = (z ∸ x) + (x ∸ y).
   Proof.
     intros. destruct (total (≤) x z).
-     rewrite (cut_minus_0 x z), cut_minus_le_trans by easy. ring.
-    rewrite (cut_minus_0 z x) by easy. ring_simplify. now auto.
+     rewrite (cut_minus_0 x z), cut_minus_le_trans by done. ring.
+    rewrite (cut_minus_0 z x) by done. ring_simplify. now auto.
   Qed.
 
   Lemma cut_minus_plus_toggle3 x₁ x₂ y₁ y₂ : x₁ ≤ y₁ → y₂ ≤ x₂
      → (y₁ ∸ x₁) + ((x₁ + x₂) ∸ (y₁ + y₂)) = (x₂ ∸ y₂) + ((y₁ + y₂) ∸ (x₁ + x₂)).
   Proof.
     intros. destruct (total (≤) (x₁ + x₂) (y₁ + y₂)).
-     rewrite (cut_minus_0 (x₁ + x₂) (y₁ + y₂)) by easy.
-     rewrite cut_minus_plus_distr by easy.
+     rewrite (cut_minus_0 (x₁ + x₂) (y₁ + y₂)) by done.
+     rewrite cut_minus_plus_distr by done.
      setoid_replace (x₂ + (y₁ + y₂)) with (y₁ + (x₂ + y₂)) by ring.
      setoid_replace (y₂ + (x₁ + x₂)) with (x₁ + (x₂ + y₂)) by ring.
      rewrite <-cut_minus_plus_rev_r. ring.
-    rewrite (cut_minus_0 (y₁ + y₂) (x₁ + x₂)) by easy.
-    rewrite cut_minus_plus_distr by easy.
+    rewrite (cut_minus_0 (y₁ + y₂) (x₁ + x₂)) by done.
+    rewrite cut_minus_plus_distr by done.
     setoid_replace (y₁ + (x₁ + x₂)) with (x₂ + (x₁ + y₁)) by ring.
     setoid_replace (x₁ + (y₁ + y₂)) with (y₂ + (x₁ + y₁)) by ring.
     rewrite <-cut_minus_plus_rev_r. ring.
@@ -160,7 +160,7 @@ Section cut_minus_properties.
   Lemma cut_minus_0_plus_toggle x : x + (0 ∸ x) = x ∸ 0.
   Proof.
     destruct (total (≤) 0 x).
-     rewrite (cut_minus_0 0 x), (cut_minus_nonneg_0_r x) by easy. ring.
+     rewrite (cut_minus_0 0 x), (cut_minus_nonneg_0_r x) by done. ring.
     rewrite (cut_minus_0 x 0), commutativity; auto.
   Qed.
 
@@ -169,7 +169,7 @@ Section cut_minus_properties.
     intros. rewrite <-!cut_minus_0_plus_toggle.
     apply (right_cancellation (+) x).
     setoid_replace (y ∸ x + (x + (0 ∸ x)) + (0 ∸ y) + x) with ((y ∸ x + x) + (x + (0 ∸ x)) + (0 ∸ y)) by ring.
-    rewrite (cut_minus_le y x) by easy. ring.
+    rewrite (cut_minus_le y x) by done. ring.
   Qed.
 
   (* * Properties of min and minus *)
@@ -230,30 +230,30 @@ Section cut_minus_default.
   Qed.
 End cut_minus_default.
 
-Set Warnings "-unsupported-attributes". (* FIXME: remove when minimal Coq version is enough *)
-
-#[global]
-Typeclasses Opaque default_cut_minus.
-
-Set Warnings "+unsupported-attributes".
-
-Section order_preserving.
-  Context `{FullPseudoSemiRingOrder A} `{!TrivialApart A} `{!CutMinusSpec A cmA} `{∀ x y : A, Decision (x = y)}
-   `{FullPseudoSemiRingOrder B} `{!TrivialApart B} `{!CutMinusSpec B cmB} `{∀ x y : B, Decision (x = y)}
-     {f : A → B} `{!OrderPreserving f} `{!SemiRing_Morphism f}.
-
-  Local Existing Instance pseudo_srorder_semiring.
-
-  Lemma preserves_cut_minus x y : f (x ∸ y) = f x ∸ f y.
-  Proof.
-    destruct (total (≤) x y) as [E|E].
-     rewrite (cut_minus_0 x y E), (cut_minus_0 (f x) (f y)).
-     apply rings.preserves_0.
-     now apply (order_preserving _).
-    apply (left_cancellation (+) (f y)). rewrite 2!(commutativity (f y)).
-    rewrite <-rings.preserves_plus.
-    rewrite (cut_minus_le x y E), (cut_minus_le (f x) (f y)).
-     reflexivity.
-    now apply (order_preserving _).
-  Qed.
-End order_preserving.
+Set Warnings "-unsupported-attributes". (* FIXME: remove when minimal Coq version is enough *)
+
+#[global]
+Typeclasses Opaque default_cut_minus.
+
+Set Warnings "+unsupported-attributes".
+
+Section order_preserving.
+  Context `{FullPseudoSemiRingOrder A} `{!TrivialApart A} `{!CutMinusSpec A cmA} `{∀ x y : A, Decision (x = y)}
+   `{FullPseudoSemiRingOrder B} `{!TrivialApart B} `{!CutMinusSpec B cmB} `{∀ x y : B, Decision (x = y)}
+     {f : A → B} `{!OrderPreserving f} `{!SemiRing_Morphism f}.
+
+  Local Existing Instance pseudo_srorder_semiring.
+
+  Lemma preserves_cut_minus x y : f (x ∸ y) = f x ∸ f y.
+  Proof.
+    destruct (total (≤) x y) as [E|E].
+     rewrite (cut_minus_0 x y E), (cut_minus_0 (f x) (f y)).
+     apply rings.preserves_0.
+     now apply (order_preserving _).
+    apply (left_cancellation (+) (f y)). rewrite 2!(commutativity (f y)).
+    rewrite <-rings.preserves_plus.
+    rewrite (cut_minus_le x y E), (cut_minus_le (f x) (f y)).
+     reflexivity.
+    now apply (order_preserving _).
+  Qed.
+End order_preserving.
diff --git a/theory/dec_fields.v b/theory/dec_fields.v
index 8f3cfa1..c4cc2fb 100644
--- a/theory/dec_fields.v
+++ b/theory/dec_fields.v
@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics   
   Coq.setoid_ring.Field Coq.setoid_ring.Ring
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace
   MathClasses.theory.fields MathClasses.theory.strong_setoids.
@@ -79,7 +79,7 @@ Proof.
    now apply dec_recip_ne_0.
   rewrite dec_recip_inverse by assumption.
   rewrite <-E, dec_recip_inverse.
-   easy.
+   done.
   apply dec_recip_ne_0_iff. rewrite E.
   now apply dec_recip_ne_0.
 Qed.
@@ -248,7 +248,7 @@ Section morphisms.
     rewrite <-preserves_mult, 2!dec_recip_inverse.
       now apply preserves_1.
      now apply injective_ne_0.
-    easy.
+    done.
   Qed.
 
   Lemma dec_recip_to_recip `{Field F2} `{!StrongSemiRing_Morphism (f : F → F2)} x Pfx :
diff --git a/theory/groups.v b/theory/groups.v
index 05f9bb2..139e127 100644
--- a/theory/groups.v
+++ b/theory/groups.v
@@ -1,6 +1,6 @@
 Require
   MathClasses.theory.setoids.
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Coq.Classes.Morphisms MathClasses.interfaces.abstract_algebra.
 
 Section semigroup_props.
@@ -22,7 +22,7 @@ Ltac group_simplify :=
     (try bottomup (hints group_simplify));
     (try bottomup (choice (hints group_cancellation) ( <- associativity ))).
 
-Ltac group := group_simplify; easy.
+Ltac group := group_simplify; done.
 
 Set Warnings "-unsupported-attributes". (* FIXME: remove when minimal Coq version is enough *)
 
diff --git a/theory/int_abs.v b/theory/int_abs.v
index ea6c595..9344af9 100644
--- a/theory/int_abs.v
+++ b/theory/int_abs.v
@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Coq.setoid_ring.Ring MathClasses.interfaces.naturals MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders
   MathClasses.orders.nat_int MathClasses.theory.integers MathClasses.theory.rings MathClasses.orders.rings.
 
@@ -120,7 +120,7 @@ Proof.
   apply (injective f). rewrite preserves_mult.
   destruct (int_abs_spec x) as [[? Ex]|[? Ex]],
      (int_abs_spec y) as [[? Ey]|[? Ey]]; rewrite Ex, Ey.
-     rewrite int_abs_nonneg. easy. now apply nonneg_mult_compat.
+     rewrite int_abs_nonneg. done. now apply nonneg_mult_compat.
     rewrite int_abs_nonpos. ring. now apply nonneg_nonpos_mult.
    rewrite int_abs_nonpos. ring. now apply nonpos_nonneg_mult.
   rewrite int_abs_nonneg. ring. now apply nonpos_mult.
diff --git a/theory/int_pow.v b/theory/int_pow.v
index 20bc70d..bbc9039 100644
--- a/theory/int_pow.v
+++ b/theory/int_pow.v
@@ -1,6 +1,6 @@
 Require
   MathClasses.theory.naturals MathClasses.orders.semirings MathClasses.orders.integers MathClasses.orders.dec_fields.
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Coq.setoid_ring.Ring Coq.setoid_ring.Field
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers
   MathClasses.interfaces.additional_operations MathClasses.interfaces.orders
@@ -132,7 +132,7 @@ Proof.
     solve_proper.
    now apply int_pow_0.
   intros n. rewrite int_pow_S, left_identity.
-   easy.
+   done.
   now apply (rings.is_ne_0 1).
 Qed.
 
@@ -173,7 +173,7 @@ Proof.
     now rewrite left_absorb.
    destruct (decide (m = 0)) as [Em|Em].
     now rewrite Em, right_absorb, 2!int_pow_0.
-   rewrite 3!int_pow_base_0; try easy.
+   rewrite 3!int_pow_base_0; try done.
    intros E. now destruct (zero_product n m E).
   revert m. apply biinduction.
     solve_proper.
@@ -188,7 +188,7 @@ Proof.
     apply (rings.left_cancellation_ne_0 (.*.) (x ^ n)).
      now apply int_pow_ne_0.
     now rewrite E.
-   easy.
+   done.
   now apply int_pow_ne_0.
 Qed.
 
@@ -263,7 +263,7 @@ Instance int_pow_exp_le:
   ∀ x : A, PropHolds (1 ≤ x) → OrderPreserving (x^).
 Proof.
   repeat (split; try apply _).
-  assert (0 < x) by (apply orders.lt_le_trans with 1; [solve_propholds | easy]).
+  assert (0 < x) by (apply orders.lt_le_trans with 1; [solve_propholds | done]).
   intros n m E.
   destruct (semirings.decompose_le E) as [z [Ea Eb]].
   rewrite Eb.
@@ -277,7 +277,7 @@ Instance int_pow_exp_lt:
   ∀ x : A, PropHolds (1 < x) → StrictlyOrderPreserving (x^).
 Proof.
   repeat (split; try apply _).
-  assert (0 < x) by (apply orders.le_lt_trans with 1; [solve_propholds | easy]).
+  assert (0 < x) by (apply orders.le_lt_trans with 1; [solve_propholds | done]).
   intros n m E.
   apply nat_int.lt_iff_plus_1_le in E.
   destruct (semirings.decompose_le E) as [z [Ea Eb]].
@@ -363,7 +363,7 @@ Section exp_preservation.
      rewrite Ex.
      destruct (decide (n = 0)) as [En|En].
       now rewrite En, rings.preserves_0, 2!int_pow_0.
-     rewrite 2!int_pow_base_0; try easy.
+     rewrite 2!int_pow_base_0; try done.
      now apply rings.injective_ne_0.
     revert n. apply biinduction.
       solve_proper.
diff --git a/theory/int_to_nat.v b/theory/int_to_nat.v
index e4251f9..318b506 100644
--- a/theory/int_to_nat.v
+++ b/theory/int_to_nat.v
@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Coq.setoid_ring.Ring MathClasses.interfaces.naturals MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders
   MathClasses.orders.nat_int MathClasses.theory.integers MathClasses.theory.rings MathClasses.orders.rings.
 
@@ -100,9 +100,9 @@ Lemma int_to_nat_mult_nonneg_l x y :
   0 ≤ x → int_to_nat Z N (x * y) = int_to_nat Z N x * int_to_nat Z N y.
 Proof.
   intros E. apply (injective f). rewrite preserves_mult. 
-  rewrite (int_to_nat_of_nonneg x) by easy.
+  rewrite (int_to_nat_of_nonneg x) by done.
   destruct (int_to_nat_spec y) as [[? Ey]|[? Ey]]; rewrite Ey, ?preserves_0.
-   rewrite int_to_nat_of_nonneg. easy. now apply nonneg_mult_compat.
+   rewrite int_to_nat_of_nonneg. done. now apply nonneg_mult_compat.
   rewrite int_to_nat_of_nonpos, preserves_0. ring. now apply nonneg_nonpos_mult.
 Qed.
 
@@ -160,13 +160,13 @@ Proof.
   repeat (split; try apply _). intros x y E.
   destruct (total (≤) 0 x).
    now apply int_to_nat_le_cancel_r, int_to_nat_le_l.
-  rewrite int_to_nat_of_nonpos. solve_propholds. easy.
+  rewrite int_to_nat_of_nonpos. solve_propholds. done.
 Qed.
 
 Lemma int_to_nat_le_back x y :
   0 ≤ y → int_to_nat Z N x ≤ int_to_nat Z N y → x ≤ y.
 Proof.
-  intros. rewrite <-(int_to_nat_of_nonneg y) by easy.
+  intros. rewrite <-(int_to_nat_of_nonneg y) by done.
   transitivity (f (int_to_nat Z N x)).
    now apply int_to_nat_le_r.
   now apply (order_preserving f).
@@ -197,13 +197,13 @@ Lemma int_to_nat_lt x y :
 Proof.
   intros Ey Exy. destruct (total (≤) 0 x).
    now apply int_to_nat_lt_cancel_r, int_to_nat_lt_l.
-  rewrite int_to_nat_of_nonpos by easy. now apply int_to_nat_pos.
+  rewrite int_to_nat_of_nonpos by done. now apply int_to_nat_pos.
 Qed.
 
 Lemma int_to_nat_lt_back x y :
   0 ≤ y → int_to_nat Z N x < int_to_nat Z N y → x < y.
 Proof.
-  intros. rewrite <-(int_to_nat_of_nonneg y) by easy.
+  intros. rewrite <-(int_to_nat_of_nonneg y) by done.
   apply le_lt_trans with (f (int_to_nat Z N x)).
    now apply int_to_nat_le_r.
   now apply (strictly_order_preserving f).
diff --git a/theory/jections.v b/theory/jections.v
index 5ef7d4e..458a460 100644
--- a/theory/jections.v
+++ b/theory/jections.v
@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   MathClasses.theory.setoids MathClasses.interfaces.abstract_algebra.
 
 Local Existing Instance injective_mor.
@@ -61,7 +61,7 @@ Global Existing Instance id_morphism.
 
 #[global]
 Instance id_injective `{Setoid A} : Injective (@id A).
-Proof. split; try apply _. easy. Qed.
+Proof. split; try apply _. done. Qed.
 #[global]
 Instance id_surjective `{Setoid A} : Surjective (@id A).
 Proof. split; try apply _. now repeat intro. Qed.
diff --git a/theory/monads.v b/theory/monads.v
index f8c01fa..d04df08 100644
--- a/theory/monads.v
+++ b/theory/monads.v
@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.functors.
 
 #[global]
@@ -134,7 +134,7 @@ Section monad.
       intros A ?? B ?? f g E1 m n E2.
       apply mon_bind_proper.
        intros x y E3. now apply mon_ret_proper, E1.
-      easy.
+      done.
      intros A ? B ? f ??? E. pose proof (setoidmor_a f). pose proof (setoidmor_b f).
      now rewrite E.
     intros A ?? ?? E. unfold join, default_mon_join.
diff --git a/theory/nat_pow.v b/theory/nat_pow.v
index f661558..45d175f 100644
--- a/theory/nat_pow.v
+++ b/theory/nat_pow.v
@@ -1,6 +1,6 @@
 Require
   MathClasses.theory.naturals.
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.interfaces.additional_operations.
 
 (* * Properties of Nat Pow *)
@@ -195,12 +195,12 @@ Section nat_pow_default.
   Instance: Proper ((=) ==> (=) ==> (=)) nat_pow_peano.
   Proof.
     intros ? ? E a ? [].
-    induction a; try easy.
+    induction a; try done.
     simpl. now rewrite IHa, E.
   Qed.
 
   Global Instance: NatPowSpec A nat nat_pow_peano.
-  Proof. split; try apply _; easy. Qed.
+  Proof. split; try apply _; done. Qed.
 
   Context `{Naturals B}.
 
@@ -214,7 +214,7 @@ Section nat_pow_default.
   Qed.
 End nat_pow_default.
 
-Set Warnings "-unsupported-attributes". (* FIXME: remove when minimal Coq version is enough *)
-
-#[global]
-Typeclasses Opaque default_nat_pow.
+Set Warnings "-unsupported-attributes". (* FIXME: remove when minimal Coq version is enough *)
+
+#[global]
+Typeclasses Opaque default_nat_pow.
diff --git a/theory/naturals.v b/theory/naturals.v
index 510a10f..3a73327 100644
--- a/theory/naturals.v
+++ b/theory/naturals.v
@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.implementations.peano_naturals MathClasses.theory.rings
   Coq.Arith.PeanoNat
   MathClasses.categories.varieties MathClasses.theory.ua_transference.
@@ -139,7 +139,7 @@ Section borrowed_from_nat.
   Proof.
     intros z E x y.
     rapply (from_nat_stmt ((z' === 0 -=> Ext _ False) -=> z' * x' === z' * y' -=> x' === y') (three_vars x y z)).
-    intro. simpl. intros. now apply (left_cancellation_ne_0 (.*.) (v () 2)). easy.
+    intro. simpl. intros. now apply (left_cancellation_ne_0 (.*.) (v () 2)). done.
   Qed.
 
   Global Instance: ∀ z : N, PropHolds (z ≠ 0) → RightCancellation (.*.) z.
diff --git a/theory/streams.v b/theory/streams.v
index f5fc3d3..25e61c8 100644
--- a/theory/streams.v
+++ b/theory/streams.v
@@ -1,7 +1,7 @@
 (* In the standard library equality on streams is defined as pointwise Leibniz equality.
     Here we prove similar results, but we use setoid equality instead. *)
 Require Export MathClasses.theory.CoqStreams.
-Require Import MathClasses.implementations.peano_naturals MathClasses.interfaces.abstract_algebra.
+Require Import MathClasses.misc.stdpp_tactics MathClasses.implementations.peano_naturals MathClasses.interfaces.abstract_algebra.
 
 Section streams.
 Context `{Setoid A}.
@@ -31,7 +31,7 @@ Proof.
   intros ? ? E.
   constructor.
    simpl. now rewrite E.
-  easy.
+  done.
 Qed.
 
 Global Instance: Proper ((=) ==> (=)) (@hd A).
@@ -49,7 +49,7 @@ Proof.
   unfold equiv, peano_naturals.nat_equiv in E1.
   rewrite E1. clear E1 n.
   induction m.
-   easy.
+   done.
   simpl. rewrite <-2!tl_nth_tl.
   now rewrite IHm.
 Qed.
@@ -104,7 +104,7 @@ Lemma EventuallyForAll_Str_nth_tl P n s :
 Proof.
   revert s.
   induction n.
-   easy.
+   done.
   intros. now apply IHn, EventuallyForAll_tl.
 Qed.
 
diff --git a/theory/strong_setoids.v b/theory/strong_setoids.v
index c79720f..29423dc 100644
--- a/theory/strong_setoids.v
+++ b/theory/strong_setoids.v
@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   MathClasses.interfaces.abstract_algebra MathClasses.theory.jections.
 
 Section contents.
@@ -151,70 +151,70 @@ End more_morphisms.
 #[global]
 Instance default_apart `{Equiv A} : Apart A | 20 := (≠).
 
-Set Warnings "-unsupported-attributes". (* FIXME: remove when minimal Coq version is enough *)
-
-#[global]
-Typeclasses Opaque default_apart.
-
-Set Warnings "+unsupported-attributes".
-
-#[global]
-Instance default_apart_trivial `{Equiv A} : TrivialApart A (Aap:=default_apart).
-Proof. red. reflexivity. Qed.
-
-(* In case we have a decidable setoid, we can construct a strong setoid. Again
-  we do not make this an instance as it will cause loops *)
-Section dec_setoid.
-  Context `{Setoid A} `{Apart A} `{!TrivialApart A} `{∀ x y, Decision (x = y)}.
-
-  (* Not Global in order to avoid loops *)
-  Instance ne_apart x y : PropHolds (x ≠ y) → PropHolds (x ≶ y).
-  Proof. rewrite trivial_apart. easy. Qed.
-
-  Instance dec_strong_setoid: StrongSetoid A.
-  Proof.
-    split; try apply _.
-       firstorder.
-      intros x y. rewrite !trivial_apart. firstorder.
-     intros x y E1 z. rewrite !trivial_apart.
-     destruct (decide (x = z)) as [E2|E2]; [|tauto].
-     right. intros E3. rewrite trivial_apart in E1. apply E1. now rewrite E2.
-    intros x y. rewrite trivial_apart. split.
-     intros E. now apply stable.
-    firstorder.
-  Qed.
-End dec_setoid.
-
-(* And a similar result for morphisms *)
-Section dec_setoid_morphisms.
-  Context `{StrongSetoid A} `{!TrivialApart A} `{StrongSetoid B}.
-
-  Instance dec_strong_morphism (f : A → B) `{!Setoid_Morphism f} :
-    StrongSetoid_Morphism f.
-  Proof.
-    split; try apply _.
-    intros x y E. apply trivial_apart, (setoids.morphism_ne f). now apply apart_ne.
-  Qed.
-
-  Context `{!TrivialApart B}.
-
-  Instance dec_strong_injective (f : A → B) `{!Injective f} :
-    StrongInjective f.
-  Proof.
-    pose proof (injective_mor f).
-    split; try apply _.
-    intros x y. rewrite !trivial_apart. now apply (injective_ne f).
-  Qed.
-
-  Context `{StrongSetoid C}.
-
-  Instance dec_strong_binary_morphism (f : A → B → C) `{!Proper ((=) ==> (=) ==> (=)) f} :
-    StrongSetoid_BinaryMorphism f.
-  Proof.
-    split; try apply _.
-    intros x₁ y₁ x₂ y₂ E1.
-    case (cotransitive E1 (f x₂ y₁)); rewrite !trivial_apart; intros E2.
-     left. intros E3. destruct (apart_ne _ _ E2). now rewrite E3.
-    right. intros E3. destruct (apart_ne _ _ E2). now rewrite E3.
-  Qed.
-End dec_setoid_morphisms.
+Set Warnings "-unsupported-attributes". (* FIXME: remove when minimal Coq version is enough *)
+
+#[global]
+Typeclasses Opaque default_apart.
+
+Set Warnings "+unsupported-attributes".
+
+#[global]
+Instance default_apart_trivial `{Equiv A} : TrivialApart A (Aap:=default_apart).
+Proof. red. reflexivity. Qed.
+
+(* In case we have a decidable setoid, we can construct a strong setoid. Again
+  we do not make this an instance as it will cause loops *)
+Section dec_setoid.
+  Context `{Setoid A} `{Apart A} `{!TrivialApart A} `{∀ x y, Decision (x = y)}.
+
+  (* Not Global in order to avoid loops *)
+  Instance ne_apart x y : PropHolds (x ≠ y) → PropHolds (x ≶ y).
+  Proof. rewrite trivial_apart. done. Qed.
+
+  Instance dec_strong_setoid: StrongSetoid A.
+  Proof.
+    split; try apply _.
+       firstorder.
+      intros x y. rewrite !trivial_apart. firstorder.
+     intros x y E1 z. rewrite !trivial_apart.
+     destruct (decide (x = z)) as [E2|E2]; [|tauto].
+     right. intros E3. rewrite trivial_apart in E1. apply E1. now rewrite E2.
+    intros x y. rewrite trivial_apart. split.
+     intros E. now apply stable.
+    firstorder.
+  Qed.
+End dec_setoid.
+
+(* And a similar result for morphisms *)
+Section dec_setoid_morphisms.
+  Context `{StrongSetoid A} `{!TrivialApart A} `{StrongSetoid B}.
+
+  Instance dec_strong_morphism (f : A → B) `{!Setoid_Morphism f} :
+    StrongSetoid_Morphism f.
+  Proof.
+    split; try apply _.
+    intros x y E. apply trivial_apart, (setoids.morphism_ne f). now apply apart_ne.
+  Qed.
+
+  Context `{!TrivialApart B}.
+
+  Instance dec_strong_injective (f : A → B) `{!Injective f} :
+    StrongInjective f.
+  Proof.
+    pose proof (injective_mor f).
+    split; try apply _.
+    intros x y. rewrite !trivial_apart. now apply (injective_ne f).
+  Qed.
+
+  Context `{StrongSetoid C}.
+
+  Instance dec_strong_binary_morphism (f : A → B → C) `{!Proper ((=) ==> (=) ==> (=)) f} :
+    StrongSetoid_BinaryMorphism f.
+  Proof.
+    split; try apply _.
+    intros x₁ y₁ x₂ y₂ E1.
+    case (cotransitive E1 (f x₂ y₁)); rewrite !trivial_apart; intros E2.
+     left. intros E3. destruct (apart_ne _ _ E2). now rewrite E3.
+    right. intros E3. destruct (apart_ne _ _ E2). now rewrite E3.
+  Qed.
+End dec_setoid_morphisms.
diff --git a/varieties/monoids.v b/varieties/monoids.v
index a6054bb..545883a 100644
--- a/varieties/monoids.v
+++ b/varieties/monoids.v
@@ -1,5 +1,5 @@
 (* To be imported qualified. *)
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics
   MathClasses.categories.categories.
 Require
@@ -122,7 +122,7 @@ Qed.
 
 #[global]
 Instance id_monoid_morphism `{Monoid A}: Monoid_Morphism (@id A).
-Proof. repeat (split; try apply _); easy. Qed.
+Proof. repeat (split; try apply _); done. Qed.
 
 (* Finally, we use these encoding/decoding functions to specialize some universal results: *)
 Section specialized.
diff --git a/varieties/semigroups.v b/varieties/semigroups.v
index da444b7..b03b236 100644
--- a/varieties/semigroups.v
+++ b/varieties/semigroups.v
@@ -1,7 +1,7 @@
 (* To be imported qualified. *)
 Require
   MathClasses.categories.varieties MathClasses.categories.product MathClasses.theory.forget_algebra MathClasses.theory.forget_variety.
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics categories.categories.
 
 Inductive op := mult.
@@ -107,7 +107,7 @@ Qed.
 
 #[global]
 Instance id_sg_morphism `{SemiGroup A}: SemiGroup_Morphism (@id A).
-Proof. repeat (split; try apply _); easy. Qed.
+Proof. repeat (split; try apply _); done. Qed.
 
 (* Finally, we use these encoding/decoding functions to specialize some universal results: *)
 Section specialized.