diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index fda9809..fe86328 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -18,16 +18,19 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.19'
+          - 'coqorg/coq:8.18'
+          - 'coqorg/coq:8.17'
           - 'coqorg/coq:8.16'
-          - 'coqorg/coq:8.15'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-coq-art.opam'
           custom_image: ${{ matrix.image }}
 
+
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme
 # https://github.com/erikmd/docker-coq-github-action-demo
diff --git a/README.md b/README.md
index b3702a9..6be21d7 100644
--- a/README.md
+++ b/README.md
@@ -10,8 +10,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [![Zulip][zulip-shield]][zulip-link]
 [![DOI][doi-shield]][doi-link]
 
-[docker-action-shield]: https://github.com/coq-community/coq-art/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/coq-community/coq-art/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/coq-community/coq-art/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/coq-art/actions/workflows/docker-action.yml
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
@@ -40,7 +40,7 @@ out of over 200 exercises from the book.
   - Yves Bertot ([**@ybertot**](https://github.com/ybertot))
   - Pierre Castéran ([**@Casteran**](https://github.com/Casteran))
 - License: [MIT License](LICENSE)
-- Compatible Coq versions: 8.15 or later (use the corresponding release for other Coq versions)
+- Compatible Coq versions: 8.16 or later (use the corresponding release for other Coq versions)
 - Additional dependencies: none
 - Coq namespace: `coqart`
 - Related publication(s):
diff --git a/ch12_modules/SRC/chap12.v b/ch12_modules/SRC/chap12.v
index 3406b03..4a54b08 100644
--- a/ch12_modules/SRC/chap12.v
+++ b/ch12_modules/SRC/chap12.v
@@ -452,16 +452,16 @@ Module Nat_Order : DEC_ORDER with Definition A := nat with Definition
 
 
   Theorem lt_le_weak : forall a b:A, lt a b -> le a b.
-  Proof lt_le_weak. 
+  Proof Nat.lt_le_incl.
   
   Theorem lt_diff : forall a b:A, lt a b -> a <> b.
   Proof.
     unfold  lt, le in |- *; intros a b H e;
-      rewrite e in H;  case (lt_irrefl b H).
+      rewrite e in H;  case (Nat.lt_irrefl b H).
   Qed.
 
   Theorem le_lt_or_eq : forall a b:A, le a b -> lt a b \/ a = b.
-  Proof le_lt_or_eq. 
+  Proof (fun a b Hle => proj1 (Nat.lt_eq_cases _ _) Hle).
 
   
   Definition lt_eq_lt_dec : forall a b:A, {lt a b} + {a = b} + {lt b a} :=
diff --git a/ch15_general_recursion/SRC/bdivspec.v b/ch15_general_recursion/SRC/bdivspec.v
index c3a0541..9f00354 100644
--- a/ch15_general_recursion/SRC/bdivspec.v
+++ b/ch15_general_recursion/SRC/bdivspec.v
@@ -1,6 +1,13 @@
 Require Export Arith.
 Require Export Lia.
 Require Export ArithRing.
+
+Lemma le_plus_minus_r : forall n m : nat, n <= m -> n + (m - n) = m.
+Proof.
+intros n m Hle.
+rewrite (Nat.add_comm n (m - n)), (Nat.sub_add n m Hle).
+reflexivity.
+Qed.
  
 Lemma sub_decrease : forall b n m:nat, n <= S b -> 0 < m -> n - m <= b.
 Proof. intros; lia. Qed.
@@ -10,11 +17,11 @@ Ltac remove_minus :=
   |  |- context [(?X1 - ?X2 + ?X3)] =>
       rewrite <- (Nat.add_comm X3); remove_minus
   |  |- context [(?X1 + (?X2 - ?X3) + ?X4)] =>
-      rewrite (plus_assoc_reverse X1 (X2 - X3)); remove_minus
+      rewrite <- (Nat.add_assoc X1 (X2 - X3)); remove_minus
   |  |- context [(?X1 + (?X2 + (?X3 - ?X4)))] =>
-      rewrite (plus_assoc X1 X2 (X3 - X4))
+      rewrite (Nat.add_assoc X1 X2 (X3 - X4))
   |  |- (_ = ?X1 + (?X2 - ?X3)) =>
-      apply (fun n m p:nat => plus_reg_l m p n) with X3;
+      apply (fun n m p:nat => proj1 (Nat.add_cancel_l m p n)) with X3;
        try rewrite (Nat.add_shuffle3 X3 X1 (X2 - X3)); 
        rewrite le_plus_minus_r
   end.
@@ -24,7 +31,7 @@ Definition bdivspec :
     n <= b -> 0 < m -> {q : nat &  {r : nat | n = m * q + r /\ r < m}}.
  fix bdivspec 1.
  {  intros b; case b.
-    -  intros n m Hle Hlt; rewrite <- (le_n_O_eq _ Hle);
+    -  intros n m Hle Hlt; rewrite (proj1 (Nat.le_0_r _) Hle);
        exists 0; exists 0; split;
        auto with arith.
        ring.
diff --git a/ch15_general_recursion/SRC/chap15.v b/ch15_general_recursion/SRC/chap15.v
index 4850cbb..e963519 100644
--- a/ch15_general_recursion/SRC/chap15.v
+++ b/ch15_general_recursion/SRC/chap15.v
@@ -33,7 +33,7 @@ Proof.
  -  intros b' Hrec m n Hleb Hlt; case (le_gt_dec n m); simpl; auto.
     intros Hle; generalize (Hrec (m-n) n);
     case (bdiv_aux b' (m-n) n); simpl; intros q r Hrec'.
-    rewrite <- plus_assoc; rewrite <- Hrec'; auto with arith.
+    rewrite <- Nat.add_assoc; rewrite <- Hrec'; auto with arith.
     lia. 
 Qed.
 
@@ -72,8 +72,6 @@ Time Eval lazy beta delta iota zeta in
 
 *)
 
-Require Import Lt.
-
 (** Also proven in Coq.Arith.Wf_nat *)
 
 Theorem lt_Acc : forall n:nat, Acc lt n.
@@ -143,7 +141,7 @@ Proof.
             (exist (div_type'' m n 0) m _)
      end); unfold div_type''; auto with arith.
   elim H_spec; intros H1 H2; split; auto.
-  rewrite (le_plus_minus n m H_n_le_m); rewrite H1; ring.
+  rewrite <- (Nat.sub_add n m H_n_le_m), H1; ring.
 Qed.
 
 Definition div :
@@ -214,7 +212,7 @@ Proof.
         rewrite Heq; auto with arith.
         rewrite Heq_test; auto.
   -  exists (0, n'); exists 0; intros k; case k.
-     + intros; elim (lt_irrefl 0); auto.
+     + intros; elim (Nat.lt_irrefl 0); auto.
      +  intros k' Hltp g; simpl; unfold div_it_F at 1.
         rewrite Heq_test; auto.
 Defined.
@@ -262,7 +260,7 @@ Proof.
  intros m; elim m using (well_founded_ind lt_wf).
  intros m' Hrec n h; rewrite div_it_fix_eqn.
  case (le_gt_dec n m'); intros H; trivial.
- pattern m' at 1; rewrite (le_plus_minus n m'); auto.
+ pattern m' at 1; rewrite <- (Nat.sub_add n m'), Nat.add_comm; auto.
  pattern (m'-n) at 1.
  rewrite Hrec with (m'-n) n h; auto with arith.
  case (div_it (m'-n) n h); simpl; auto with arith.
@@ -351,7 +349,7 @@ Proof.
  intros p l Hle.
  lazy beta iota zeta delta [two_power log_domain_inv log];
   fold log two_power.
- apply le_trans with (2 * S (div2 p)); auto with arith.
+ apply Nat.le_trans with (2 * S (div2 p)); auto with arith.
  generalize (double_div2_le (S (S p))); simpl;intro;lia.
 Qed.
 
diff --git a/ch15_general_recursion/SRC/cubic.v b/ch15_general_recursion/SRC/cubic.v
index 3289ea8..24867b8 100644
--- a/ch15_general_recursion/SRC/cubic.v
+++ b/ch15_general_recursion/SRC/cubic.v
@@ -2,7 +2,14 @@ Require Export Arith.
 Require Export ArithRing.
 Require Export Lia.
 Require Export Wf_nat.
- 
+
+Lemma le_plus_minus_r : forall n m : nat, n <= m -> n + (m - n) = m.
+Proof.
+intros n m Hle.
+rewrite (Nat.add_comm n (m - n)), (Nat.sub_add n m Hle).
+reflexivity.
+Qed.
+
 Definition div8_spec:
  forall n,  ({q : nat & {r : nat | n = 8 * q + r /\ r < 8}}).
 Proof.
diff --git a/ch15_general_recursion/SRC/div_it_companion2.v b/ch15_general_recursion/SRC/div_it_companion2.v
index f51d262..67f974c 100644
--- a/ch15_general_recursion/SRC/div_it_companion2.v
+++ b/ch15_general_recursion/SRC/div_it_companion2.v
@@ -21,7 +21,7 @@ Proof.
 intros m; induction m  as [m' Hrec]  using (well_founded_ind lt_wf).
 intros  n h; rewrite div_it_fix_eqn.
 case (le_gt_dec n m'); intros H; trivial.
-pattern m' at 1; rewrite (le_plus_minus n m'); auto.
+pattern m' at 1; rewrite <- (Nat.sub_add n m' H), Nat.add_comm; auto.
 pattern (m' - n) at 1; rewrite Hrec with (m' - n) n h; auto with arith.
 case (div_it (m' - n) n h); simpl; auto with arith.
 Qed.
diff --git a/ch15_general_recursion/SRC/log2_function.v b/ch15_general_recursion/SRC/log2_function.v
index 5e1c9d5..455a746 100644
--- a/ch15_general_recursion/SRC/log2_function.v
+++ b/ch15_general_recursion/SRC/log2_function.v
@@ -83,7 +83,7 @@ Proof.
       intro H.
       case_eq (exp2 p).
       * intro H0; destruct (exp2_positive p);auto.
-      * intros n H0;  rewrite H0 in H.  elimtype False; lia.   
+      * intros n H0;  rewrite H0 in H.  exfalso; lia.   
  - intros p H;  destruct p. 
    +  simpl in H;  subst n; contradiction. 
    +  simpl in H; rewrite (IHn0 p); auto. 
diff --git a/ch15_general_recursion/SRC/log2_it.v b/ch15_general_recursion/SRC/log2_it.v
index 2a9a767..c4e3296 100644
--- a/ch15_general_recursion/SRC/log2_it.v
+++ b/ch15_general_recursion/SRC/log2_it.v
@@ -102,7 +102,7 @@ intros x; case x.
       elim (div2_eq (S (S p))).
       lia.
       lia.
-      apply le_lt_trans with (2 * div2 (S (S p)) + 1).
+      apply Nat.le_lt_trans with (2 * div2 (S (S p)) + 1).
       elim (div2_eq (S (S p))).
       lia.
       lia.
diff --git a/ch15_general_recursion/SRC/sqrt.v b/ch15_general_recursion/SRC/sqrt.v
index 7e93beb..8945938 100644
--- a/ch15_general_recursion/SRC/sqrt.v
+++ b/ch15_general_recursion/SRC/sqrt.v
@@ -1,6 +1,13 @@
 Require Export Arith.
 Require Export ArithRing.
 Require Export Lia.
+
+Lemma le_plus_minus_r : forall n m : nat, n <= m -> n + (m - n) = m.
+Proof.
+intros n m Hle.
+rewrite (Nat.add_comm n (m - n)), (Nat.sub_add n m Hle).
+reflexivity.
+Qed.
  
 Ltac CaseEq f := generalize (refl_equal f); 
     pattern f at -1 in |- *; case f.
@@ -77,9 +84,9 @@ Ltac remove_minus :=
   |  |- context [(?X1 - ?X2 + ?X3)] =>
       rewrite <- (Nat.add_comm X3); remove_minus
   |  |- context [(?X1 + (?X2 - ?X3) + ?X4)] =>
-      rewrite (plus_assoc_reverse X1 (X2 - X3)); remove_minus
+      rewrite <- (Nat.add_assoc X1 (X2 - X3)); remove_minus
   |  |- context [(?X1 + (?X2 + (?X3 - ?X4)))] =>
-      rewrite (plus_assoc X1 X2 (X3 - X4))
+      rewrite (Nat.add_assoc X1 X2 (X3 - X4))
   |  |- (_ = ?X1 + (?X2 - ?X3)) =>
       apply (fun n m p:nat => Nat.add_cancel_l m p n) with X3;
        try rewrite (Nat.add_shuffle3 X3 X1 (X2 - X3)); 
@@ -124,7 +131,7 @@ Proof.
 (* When the bound is zero, if n is lower than the bound, it
   is also 0, it is only a matter of computation to check the
   equality. *)
- intros n Hle; rewrite <- (le_n_O_eq _ Hle); simpl in |- *; auto.
+ intros n Hle; rewrite (proj1 (Nat.le_0_r _) Hle); simpl in |- *; auto.
 
  (*We limit simplification to the bsqrt function. *)
  intros b' Hrec n Hle; cbv beta iota zeta delta [bsqrt] in |- *;
@@ -152,7 +159,7 @@ Theorem bsqrt_rem :
    let (s, r) := bsqrt n b in n < (s + 1) * (s + 1).
 Proof.
  intros b; elim b.
- -  intros n Hle; rewrite <- (le_n_O_eq _ Hle); 
+ -  intros n Hle; rewrite (proj1 (Nat.le_0_r _) Hle); 
   simpl in |- *; auto with arith.
 
  (*We limit simplification to the bsqrt function. *)
@@ -173,7 +180,7 @@ Proof.
    the case analysis on this function call. *)
  case (le_gt_dec (4 * s' + 1) (4 * r' + r)).
  *  intros Hle' Heq'; rewrite Heq.
-    apply lt_le_trans with (4 * S q' + 4).
+    apply Nat.lt_le_trans with (4 * S q' + 4).
     auto with arith.
      replace ((2 * s' + 1 + 1) * (2 * s' + 1 + 1)) with
      (4 * ((s' + 1) * (s' + 1))).
diff --git a/ch15_general_recursion/SRC/sqrt_nat_wf.v b/ch15_general_recursion/SRC/sqrt_nat_wf.v
index 39995e9..63b80eb 100644
--- a/ch15_general_recursion/SRC/sqrt_nat_wf.v
+++ b/ch15_general_recursion/SRC/sqrt_nat_wf.v
@@ -3,6 +3,13 @@ Require Export ArithRing.
 Require Export Lia.
 Require Export Compare_dec.
 Require Export Wf_nat.
+
+Lemma le_plus_minus_r : forall n m : nat, n <= m -> n + (m - n) = m.
+Proof.
+intros n m Hle.
+rewrite (Nat.add_comm n (m - n)), (Nat.sub_add n m Hle).
+reflexivity.
+Qed.
  
 Definition div4_spec:
  forall (n : nat),  ({q : nat & {r : nat | n = 4 * q + r /\ r < 4}}).
@@ -48,9 +55,9 @@ refine (fun n sqrt_nat =>
     * replace (4 * (s' * s' + r'') + r') with ((4 * s') * s' + (4 * r'' + r')).
       replace (((2 * s' + 1) + 1) * ((2 * s' + 1) + 1))
       with ((4 * s') * s' + (8 * s' + 4)).
-      apply plus_lt_compat_l.
+      apply Nat.add_lt_mono_l.
       assert (H: r'' < 2 * s' + 1).
-      { apply plus_lt_reg_l with (s' * s').
+      { apply Nat.add_lt_mono_l with (s' * s').
         rewrite <- Heq'.
         replace (s' * s' + (2 * s' + 1)) with ((s' + 1) * (s' + 1)).
         assumption.
diff --git a/ch16_proof_by_reflection/SRC/chap16.v b/ch16_proof_by_reflection/SRC/chap16.v
index 0307680..4492e2d 100644
--- a/ch16_proof_by_reflection/SRC/chap16.v
+++ b/ch16_proof_by_reflection/SRC/chap16.v
@@ -27,10 +27,10 @@ Theorem divisor_smaller :
 Proof.
  intros m p Hlt; case p.
  -  intros q Heq; rewrite Heq in Hlt; rewrite Nat.mul_comm in Hlt.
-    elim (lt_irrefl 0);exact Hlt.
+    elim (Nat.lt_irrefl 0);exact Hlt.
  -  intros p' q; case q.
     +  intros Heq; rewrite Heq in Hlt.
-       elim (lt_irrefl 0);exact Hlt.
+       elim (Nat.lt_irrefl 0);exact Hlt.
     +  intros q' Heq; rewrite Heq.
        rewrite Nat.mul_comm; simpl; auto with arith.
 Qed.
@@ -73,10 +73,10 @@ Theorem Zabs_nat_0 : forall x:Z, Z.abs_nat x = 0 -> (x = 0)%Z.
 Proof.
  intros x; case x.
  -  simpl; auto.
- -  intros p Heq; elim (lt_irrefl 0).
+ -  intros p Heq; elim (Nat.lt_irrefl 0).
     pattern 0 at 2; rewrite <- Heq.
     simpl; apply lt_O_nat_of_P.
- -  intros p Heq; elim (lt_irrefl 0).
+ -  intros p Heq; elim (Nat.lt_irrefl 0).
     pattern 0 at 2; rewrite <- Heq.
     simpl; apply lt_O_nat_of_P.
 Qed.
@@ -207,7 +207,7 @@ Proof.
  -  intros Hcp (k, (Hne1, (Hne1bis, (q, Heq))));
    rewrite Nat.mul_comm in Heq.
     assert (Hle' : k < 1).
-   +  elim (le_lt_or_eq k 1); try(intuition; fail).
+   +  elim (proj1 (Nat.lt_eq_cases k 1)); try(intuition; fail).
       apply divisor_smaller with (2:= Heq); auto.
    + case_eq k.
      intros Heq'; rewrite Heq' in Heq; simpl in Heq; discriminate Heq.
@@ -249,7 +249,7 @@ Time Qed.
 Theorem reflection_test :
  forall x y z t u:nat, x+(y+z+(t+u)) = x+y+(z+(t+u)).
 Proof.
- intros; repeat rewrite plus_assoc; auto.
+ intros; repeat rewrite Nat.add_assoc; auto.
 Qed.
 
 Inductive bin : Set := node : bin->bin->bin | leaf : nat->bin.
@@ -285,7 +285,7 @@ Theorem flatten_aux_valid :
 Proof.
  intros t; elim t; simpl; auto.
  intros t1 IHt1 t2 IHt2 t'; rewrite <- IHt1; rewrite <- IHt2.
- rewrite plus_assoc; trivial.
+ rewrite Nat.add_assoc; trivial.
 Qed.
 
 Theorem flatten_valid : forall t:bin, bin_nat t = bin_nat (flatten t).
diff --git a/ch16_proof_by_reflection/SRC/prime_sqrt.v b/ch16_proof_by_reflection/SRC/prime_sqrt.v
index d860638..6797073 100644
--- a/ch16_proof_by_reflection/SRC/prime_sqrt.v
+++ b/ch16_proof_by_reflection/SRC/prime_sqrt.v
@@ -122,17 +122,17 @@ Theorem test_odds_correct :
 Proof.
  induction n.
  -  intros x p Hp1 H1ltx Hn q Hint.
-    elimtype False;  lia.
+    exfalso;  lia.
   - intros x p Hp H1ltx; simpl (test_odds (S n) p (Z_of_nat x));
     intros Htest q (H1ltq, Hqle).
     case_eq (test_odds n (p -2) (Z_of_nat x)).
     + intros Htest'true.
       rewrite Htest'true in Htest.
       unfold divides_bool in Htest.
-      elim (le_lt_or_eq q (2*S n + 1)%nat Hqle).
+      elim (proj1 (Nat.lt_eq_cases q (2*S n + 1)%nat) Hqle).
       *  intros Hqlt.
          assert (Hqle': (q <= (2* S n))%nat) by  lia.
-         elim (le_lt_or_eq q (2 * S n)%nat Hqle').
+         elim (proj1 (Nat.lt_eq_cases q (2 * S n)%nat) Hqle').
          replace (2*S n)%nat with (2*n +2)%nat.
          intros Hqlt'.
          assert (Hqle'' : (q <= 2*n +1)%nat) by lia.
@@ -218,7 +218,7 @@ Proof.
        split.
        case_eq k.
        intros Hk0; rewrite Hk0 in Heq; rewrite Heq in H1ltn;
-       rewrite mult_0_r in H1ltn; lia.
+       rewrite Nat.mul_0_r in H1ltn; lia.
        intros; unfold Z.lt; simpl; auto.
        lia.
        rewrite Zmult_comm; rewrite <- inj_mult; rewrite Heq;auto.
diff --git a/ch16_proof_by_reflection/SRC/verif_divide.v b/ch16_proof_by_reflection/SRC/verif_divide.v
index 71f42bb..d6184c2 100644
--- a/ch16_proof_by_reflection/SRC/verif_divide.v
+++ b/ch16_proof_by_reflection/SRC/verif_divide.v
@@ -32,10 +32,10 @@ Theorem divisor_smaller :
 Proof.
  intros m p Hlt; case p.
  -  intros q Heq; rewrite Heq in Hlt; rewrite Nat.mul_comm in Hlt.
-     elim (lt_irrefl 0);exact Hlt.
+     elim (Nat.lt_irrefl 0);exact Hlt.
  -  intros p' q; case q.
     +  intros Heq; rewrite Heq in Hlt.
-       elim (lt_irrefl _ Hlt).
+       elim (Nat.lt_irrefl _ Hlt).
     + intros q' Heq; rewrite Heq.
       rewrite Nat.mul_comm; simpl; auto with arith.
 Qed.
@@ -44,10 +44,10 @@ Theorem Zabs_nat_0 : forall x:Z, Z.abs_nat x = 0 -> (x = 0)%Z.
 Proof.
  intros x; case x.
  -  simpl; auto.
- -  intros p Heq; elim (lt_irrefl 0).
+ -  intros p Heq; elim (Nat.lt_irrefl 0).
     pattern 0 at 2; rewrite <- Heq.
     simpl; apply lt_O_nat_of_P.
- -  intros p Heq; elim (lt_irrefl 0).
+ -  intros p Heq; elim (Nat.lt_irrefl 0).
     pattern 0 at 2; rewrite <- Heq.
     simpl; apply lt_O_nat_of_P.
 Qed.
@@ -157,7 +157,7 @@ Proof.
  unfold lt; intros p Hle; elim Hle.
  -  intros Hcp (k, (Hne1, (Hne1bis, (q, Heq)))); rewrite Nat.mul_comm in Heq.
     assert (Hle' : k < 1).
-    +  elim (le_lt_or_eq k 1); try(intuition; fail).
+    +  elim (proj1 (Nat.lt_eq_cases k 1)); try(intuition; fail).
        apply divisor_smaller with (2:= Heq); auto.
     +  case_eq k.
        *  intros Heq'; rewrite Heq' in Heq; simpl in Heq; discriminate Heq.
diff --git a/ch2_types_expressions/SRC/Zbtree.v b/ch2_types_expressions/SRC/Zbtree.v
index ebf2378..f753e2f 100644
--- a/ch2_types_expressions/SRC/Zbtree.v
+++ b/ch2_types_expressions/SRC/Zbtree.v
@@ -15,12 +15,10 @@ match t with
 | bnode _ t1 t2 => 1 + size t1 + size t2
 end.
 
-Require Export Max.
-
 Fixpoint height (t:Zbtree) : nat :=
 match t with 
 | leaf => 0
-| bnode _ t1 t2 => 1 + max (height t1 ) (height t2)
+| bnode _ t1 t2 => 1 + Nat.max (height t1 ) (height t2)
 end.
 
 Fixpoint mirror (t:Zbtree) : Zbtree :=
diff --git a/ch5_everydays_logic/SRC/chap5.v b/ch5_everydays_logic/SRC/chap5.v
index 4a331c3..c7290fc 100644
--- a/ch5_everydays_logic/SRC/chap5.v
+++ b/ch5_everydays_logic/SRC/chap5.v
@@ -56,7 +56,7 @@ Lemma mult_le_compat_r : forall m n p:nat, le n p -> le (n * m) (p * m).
 Proof.
  intros m n p H; rewrite (Nat.mul_comm n m); 
    rewrite (Nat.mul_comm p m).
- apply mult_le_compat_l; trivial.
+ apply Nat.mul_le_mono_l; trivial.
 Qed.
 
 
@@ -66,7 +66,7 @@ Proof.
  intros a b c d H H0.  
  apply Nat.le_trans with (m := c * b).
  - apply mult_le_compat_r; assumption.
- - apply mult_le_compat_l; assumption.
+ - apply Nat.mul_le_mono_l; assumption.
 Qed.
 
 
@@ -78,7 +78,7 @@ Lemma le_mult_mult' :
 Proof.
  intros a b c d H H0.  
  eapply Nat.le_trans.
- - eapply mult_le_compat_l.
+ - eapply Nat.mul_le_mono_l.
    eexact H0.
  -  now apply mult_le_compat_r.
 Qed.   
@@ -232,9 +232,9 @@ Proof.
  intros n  H H0.
  rewrite <- (le_lt_S_eq 2 n).
  - reflexivity.  
- -  apply  plus_le_reg_l with (p := 6).  
+ -  apply  Nat.add_le_mono_l with (p := 6).  
     rewrite Nat.add_comm in H; auto with arith.
- - apply   plus_lt_reg_l with (p:= 3); auto with arith.
+ - apply Nat.add_lt_mono_l with (p:= 3); auto with arith.
 Qed.
 
 (** A shorter proof ...
diff --git a/ch5_everydays_logic/SRC/plus_permute2.v b/ch5_everydays_logic/SRC/plus_permute2.v
index ddc2baa..94384b3 100644
--- a/ch5_everydays_logic/SRC/plus_permute2.v
+++ b/ch5_everydays_logic/SRC/plus_permute2.v
@@ -3,9 +3,9 @@ Require Import Arith.
 Theorem plus_permute2 : forall n m p:nat, n + m + p = n + p + m.
 Proof.
  intros n m p.
- rewrite plus_assoc_reverse.
+ rewrite <- Nat.add_assoc.
  pattern (m + p); rewrite Nat.add_comm.
- rewrite plus_assoc_reverse; reflexivity.
+ rewrite <- Nat.add_assoc; reflexivity.
 Qed.
 
 
diff --git a/ch6_inductive_data/SRC/erato.v b/ch6_inductive_data/SRC/erato.v
index 7f91187..5de418c 100644
--- a/ch6_inductive_data/SRC/erato.v
+++ b/ch6_inductive_data/SRC/erato.v
@@ -1,4 +1,3 @@
-
 Require Import List.
 Require Import Arith.
 
@@ -87,7 +86,7 @@ Proof.
   + intros p'; repeat rewrite <- mult_n_Sm.
     repeat rewrite <- (Nat.add_comm m).
     intros Hlt; assert (Hlt' : m*n' < m* p').
-    *  apply plus_lt_reg_l with m; auto.
+    *  apply Nat.add_lt_mono_l with m; auto.
     * auto with arith.
 Qed.
 
@@ -197,8 +196,8 @@ Theorem divides_dec_aux :
 Proof.
   intros k; elim k.
   -  intros n p Hle; left; exists 0; rewrite Nat.mul_comm; simpl; 
-       symmetry; apply le_n_O_eq; auto.
-  - intros k' Hrec n p Hlt; elim (le_lt_or_eq n (S k')).
+     apply (proj1 (Nat.le_0_r _)); auto.
+  - intros k' Hrec n p Hlt; elim (proj1 (Nat.lt_eq_cases n (S k')) Hlt).
     + auto with arith.
     + intros Heq; rewrite Heq.
       case p.
@@ -214,7 +213,7 @@ Proof.
            apply nat_compare_Lt_lt; auto.
            elim (Hrec (minus (S k') (S p')) (S p')).
            ++ intros (q, Heq'); left; exists (S q).
-              rewrite (le_plus_minus (S p') (S k')).
+              rewrite <- (Nat.sub_add (S p') (S k')), Nat.add_comm.
               ** rewrite Heq'.
                  repeat rewrite (Nat.mul_comm (S p')).
                  reflexivity.
@@ -225,8 +224,8 @@ Proof.
                intros q; case q.
                **  rewrite Nat.mul_comm;  simpl; intros; discriminate.
                **  intros q' Heq'; exists q'.
-                   apply plus_reg_l with (S p').
-                   rewrite le_plus_minus_r.
+                   apply Nat.add_cancel_l with (S p').
+                   rewrite Nat.add_comm, Nat.sub_add.
                    { rewrite Heq'.
                      rewrite Nat.add_comm; rewrite mult_n_Sm; reflexivity.
                    }
@@ -237,10 +236,9 @@ Proof.
             { apply nat_compare_Gt_gt; auto. }
             right; intros Hdiv; elim Hdiv; intros q; case q.
             ++  rewrite Nat.mul_comm; simpl; intros; discriminate.
-            ++ intros q' Heq'; elim (lt_not_le _ _ Hlt').
+            ++ intros q' Heq'; elim (proj1 (Nat.lt_nge _ _) Hlt').
                rewrite Heq'.
                rewrite Nat.mul_comm; simpl; auto with arith.
-    +  trivial.
 Qed.
 
 
@@ -270,10 +268,10 @@ Proof.
      --  intros; right; right; split.
          ++ auto.
          ++ intros (p, ((Hpgt1, Hplt1),_)).
-            elim (lt_irrefl 1); apply lt_trans with p;auto.
+            elim (Nat.lt_irrefl 1); apply Nat.lt_trans with p;auto.
      -- intros k''; case k''.
         ++ intros; right; right; split; auto; intros (p, ((Hpgt1, Hplt2),_)).
-           elim (lt_irrefl p); apply le_lt_trans with 1; auto with arith.
+           elim (Nat.lt_irrefl p); apply Nat.le_lt_trans with 1; auto with arith.
         ++ intros k''' Hrec; case (divides_dec_aux n n (S (S k'''))).
            ** auto with arith.
            ** intros Hdiv; right; left; exists (S (S k'''));
@@ -288,7 +286,7 @@ Proof.
                     intros (p, ((Hpgt1, Hplt), Hex)).
                   assert (Hple : p <= S (S k''')).
                   { auto with arith. }
-                  elim (le_lt_or_eq _ _ Hple).
+                  elim (proj1 (Nat.lt_eq_cases _ _) Hple).
                   intros Hplt'.
                   elim Hnodiv; exists p; repeat split; auto with arith.
                   intros Hpeq.
@@ -311,12 +309,12 @@ Theorem div_by_prime_aux :
 Proof.
  intros k; elim k.
  -  intros n Hle Hlt Hn.
-    elim (lt_asym 1 0). 
+    elim (Nat.lt_asymm 1 0). 
   +  apply Nat.lt_le_trans with n; assumption.
   + auto with arith.
  -  intros k' Hrec n Hle Hlt Hn.
-    elim (le_lt_or_eq n (S k')).
-    +  intros Hle'; apply Hrec; auto with arith.
+    elim (proj1 (Nat.lt_eq_cases n (S k')) Hle).
+    + intros Hle'; apply Hrec; auto with arith.
     + elim Hn; intros p ((Hpgt1, Hpltn),(q,Heq)).
       intros HneqSk'.
       elim (prime_dec p).
@@ -324,22 +322,21 @@ Proof.
      --  intros Hpeq0.
          rewrite Hpeq0 in Hpgt1; elim (Nat.nlt_0_r 1); assumption.
      -- intros Hpeq1;
-          rewrite Hpeq1 in Hpgt1; elim (lt_irrefl 1); assumption.
+          rewrite Hpeq1 in Hpgt1; elim (Nat.lt_irrefl 1); assumption.
     *  intros Hpdec; elim Hpdec.
        -- intros Hexp.
           elim (Hrec p); auto with arith.
           ++ intros p' ((Hp'gt1,Hp'ltp), (Hpr,(q', Heq'))).
              exists p'.
              split;[split|split]; auto with arith.
-             ** apply lt_trans with p; auto with arith.
+             ** apply Nat.lt_trans with p; auto with arith.
              **  exists (q' * q).
-                 rewrite mult_assoc.
+                 rewrite Nat.mul_assoc.
                  rewrite Heq; rewrite Heq'; trivial.
           ++  unfold lt in Hpltn.
               rewrite HneqSk' in Hpltn; auto with arith.
        --  exists p;split;[split|split]; auto with arith.
            exists q; auto with arith.
-    + trivial.
 Qed.
 
 Theorem div_by_prime :
@@ -409,12 +406,12 @@ Theorem interval_eq :
   forall p q q', p*q'-p < p*q <= p*q' -> q=q'.
 Proof.
   intros p; case p.
-  -  simpl; intros q q' (Hlt, Hle); elim (lt_irrefl 0);assumption.
+  -  simpl; intros q q' (Hlt, Hle); elim (Nat.lt_irrefl 0);assumption.
   - intros p' q q' (Hlt, Hle).
-    apply le_antisym.
-    + apply mult_S_le_reg_l with p'; auto.
+    apply Nat.le_antisymm.
+    + apply (Nat.mul_le_mono_pos_l _ _ (S p')); [apply Nat.lt_0_succ|auto].
     + assert (Hlt' : (q' - 1)*S p' < S p' * q).
-     { rewrite mult_minus_distr_r.
+     { rewrite Nat.mul_sub_distr_r.
        rewrite Nat.mul_1_l.
        rewrite (Nat.mul_comm q').
        assumption.
@@ -423,7 +420,7 @@ Proof.
      generalize (mult_lt_reg_l _ _ _ Hlt').
      case q'; simpl.
      * auto with arith.
-       * intros n; rewrite <- minus_n_O; auto with arith.
+       * intros n; rewrite Nat.sub_0_r; auto with arith.
 Qed.
 
 
@@ -440,7 +437,7 @@ Proof.
  -  intros Hkeq0or1;elim Hkeq0or1.
     + intros Hkeq0.
       rewrite Hkeq0 in Hkgt1; elim (Nat.nlt_0_r 1); assumption.
-    + intros Hkeq1; rewrite Hkeq1 in Hkgt1; elim (lt_irrefl 1); assumption.
+    + intros Hkeq1; rewrite Hkeq1 in Hkgt1; elim (Nat.lt_irrefl 1); assumption.
 - intros Hpdec; elim Hpdec.
   + intros Hexdiv.
     generalize (div_by_prime _ Hkgt1 Hexdiv).
@@ -552,16 +549,15 @@ Proof.
                  generalize (nat_compare_eq _ _ Htwc) ||
                  generalize (nat_compare_Gt_gt _ _ Htwc));
                 auto with arith. (* ICI *)
-      *  intros Heq2; rewrite Heq2; rewrite Nat.add_comm; rewrite minus_plus;
-           auto with arith.
+      *  intros Heq2; rewrite Heq2; rewrite Nat.add_sub; auto with arith.
       * intros Heq2; rewrite Heq2; unfold all_greater_than_one in Hal;
           generalize (Hal nil l0 p n (refl_equal _)); intros Hpgt1.
         pattern n at 1; rewrite plus_n_O; rewrite plus_n_Sm;
-          apply plus_le_compat; auto with arith.
-      * rewrite Nat.add_comm; rewrite minus_plus; auto with arith.
+          apply Nat.add_le_mono; auto with arith.
+      * rewrite Nat.add_sub; auto with arith.
       *  generalize (Hal nil l0 p n (refl_equal _)); intros Hpgt1.
          intros Hkltn; pattern k at 1; rewrite plus_n_O; rewrite plus_n_Sm;
-           apply plus_le_compat; auto with arith.
+           apply Nat.add_le_mono; auto with arith.
     + generalize (all_intervals_transmit _ _ _ Hai); intros Hai'.
       generalize (all_greater_than_one_transmit _ _ Hal); intros Hal'.
       simpl; clear l1; intros fst_elem l1 l2 p' n' Heq; generalize Hup;
@@ -708,7 +704,7 @@ Proof.
       split;[idtac | split; [idtac | split;[idtac|split;[idtac|split]]]];
         try (intros l1 l2 p n Heq; elim (absurd_decompose_list _ _ _ _ Heq)).
       intros n Hle1 ((Hnneq0, Hnneq1),_); elim Hnneq1.
-      elim Hle1; intros; apply (le_antisym n 1); auto with arith.
+      elim Hle1; intros; apply (Nat.le_antisymm n 1); auto with arith.
   - 
     intros k' Hrec l Hps.
     change ((let (l', b) := 
@@ -758,7 +754,7 @@ Proof.
         -- intuition.
         -- elim Hint.
            intros Hngt0 Hnlek.
-           elim (le_lt_or_eq _ _ Hnlek).
+           elim (proj1 (Nat.lt_eq_cases _ _) Hnlek).
            ++ auto with arith; fail.
            ++ intros Hn'; injection Hn'.
               intros Hn; rewrite Hn in Hpr; elim Hpr.
@@ -787,7 +783,7 @@ Proof.
         -- split.
            ++ rewrite <- Hps.
               intros n (Hpos, Hle) Hpr.
-              elim (le_lt_or_eq _ _ Hle).
+              elim (proj1 (Nat.lt_eq_cases _ _) Hle).
               ** intros Hlt; elim (Hapf n); auto with arith.
                  intros l'1 (l'2, (p, Heq2));
                    exists ((S (S k'), 2*S(S k'))::l'1); exists l'2; exists p.
@@ -799,7 +795,8 @@ Proof.
               ** rewrite <- Hps; apply all_intervals_add; auto with arith.
                  split.
                  { simpl.
-                   rewrite minus_plus.
+                   rewrite Nat.add_comm.
+                   rewrite Nat.add_sub.
                    rewrite <- plus_n_O.
                    auto with arith.
                  }
diff --git a/ch7_tactics_automation/SRC/chap7.v b/ch7_tactics_automation/SRC/chap7.v
index a5afccd..6291a70 100644
--- a/ch7_tactics_automation/SRC/chap7.v
+++ b/ch7_tactics_automation/SRC/chap7.v
@@ -7,7 +7,7 @@ Section bad_proof_example_for_Induction1.
   Theorem le_plus_minus' : forall n m:nat, m <= n -> n = m+(n-m).
   Proof.
     intros n m H;  induction n. 
-    -   rewrite <- le_n_O_eq with (1 := H); simpl; trivial. 
+    -   rewrite (proj1 (Nat.le_0_r _) H); simpl; trivial. 
     - (* dead end *) 
   Abort.
 
@@ -18,7 +18,7 @@ Theorem lazy_example : forall n:nat, (S n) + 0 = S n.
 Proof.
   intros n; lazy beta iota zeta delta. 
   fold plus.
-  rewrite plus_0_r; reflexivity.
+  rewrite Nat.add_0_r; reflexivity.
 Qed.
 
 #[export] Hint  Extern  4 (_ <> _) => discriminate : core.
@@ -79,8 +79,8 @@ Proof.
   subst a.
   subst.
   lazy delta [mult] iota zeta beta; 
-    rewrite  plus_0_r; 
-    repeat rewrite plus_assoc_reverse;
+    rewrite  Nat.add_0_r; 
+    repeat rewrite <- Nat.add_assoc;
     trivial.
 Qed.
 
@@ -286,7 +286,7 @@ Section primes.
     end.
   Open Scope nat_scope.
 
-  #[local] Hint Resolve lt_O_Sn : core.
+  #[local] Hint Resolve Nat.lt_0_succ : core.
 
   Ltac check_lt_not_divides :=
     match goal with
diff --git a/ch7_tactics_automation/SRC/primes_hyps.v b/ch7_tactics_automation/SRC/primes_hyps.v
index 098563e..e0990e7 100644
--- a/ch7_tactics_automation/SRC/primes_hyps.v
+++ b/ch7_tactics_automation/SRC/primes_hyps.v
@@ -51,7 +51,7 @@ Proof.
  intro; absurd (0 < 0); auto with arith.
  intros n0 Hn0 H1.
  elim H1; intros q Hq.
- rewrite mult_0_r in Hq; discriminate Hq.
+ rewrite Nat.mul_0_r in Hq; discriminate Hq.
  lia.
 Qed.
   
diff --git a/ch8_inductive_predicates/SRC/frobenius.v b/ch8_inductive_predicates/SRC/frobenius.v
index 8524d26..8d1b525 100644
--- a/ch8_inductive_predicates/SRC/frobenius.v
+++ b/ch8_inductive_predicates/SRC/frobenius.v
@@ -17,7 +17,7 @@ Proof.
       replace (3 * (p' - 3) + 5 * 2) 
         with    (S (3 * 3 + 3 * (p' - 3)))
         by  lia.
-      rewrite <- mult_plus_distr_l.
-      rewrite le_plus_minus_r; auto.
-   +   exists (p'+2), q'; rewrite H;  ring.
+      rewrite <- Nat.mul_add_distr_l.
+      rewrite (Nat.add_comm 3), Nat.sub_add; auto.
+   + exists (p'+2), q'; rewrite H;  ring.
 Qed.
diff --git a/coq-coq-art.opam b/coq-coq-art.opam
index c58274a..6725847 100644
--- a/coq-coq-art.opam
+++ b/coq-coq-art.opam
@@ -20,7 +20,7 @@ out of over 200 exercises from the book."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.15" & < "8.18~") | (= "dev")}
+  "coq" {(>= "8.16" & < "8.20") | (= "dev")}
 ]
 
 tags: [
diff --git a/meta.yml b/meta.yml
index 8f6cdd0..24a3d82 100644
--- a/meta.yml
+++ b/meta.yml
@@ -40,13 +40,15 @@ license:
   identifier: MIT
 
 supported_coq_versions:
-  text: 8.15 or later (use the corresponding release for other Coq versions)
-  opam: '{(>= "8.15" & < "8.18~") | (= "dev")}'
+  text: 8.16 or later (use the corresponding release for other Coq versions)
+  opam: '{(>= "8.16" & < "8.20") | (= "dev")}'
 
 tested_coq_opam_versions:
 - version: dev
+- version: '8.19'
+- version: '8.18'
+- version: '8.17'
 - version: '8.16'
-- version: '8.15'
 
 namespace: coqart
 
diff --git a/tutorial_type_classes/SRC/Monoid_prog.v b/tutorial_type_classes/SRC/Monoid_prog.v
index 03199d3..51413a4 100644
--- a/tutorial_type_classes/SRC/Monoid_prog.v
+++ b/tutorial_type_classes/SRC/Monoid_prog.v
@@ -6,7 +6,6 @@ Set Implicit Arguments.
 
 Require Import ZArith Arith.
 Require Import Mat.
-Require Import Div2.
 Require Import Program.
 
 Class Monoid {A:Type}(dot : A -> A -> A)(one : A) : Type := {