diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 2dc8190..e11c8b9 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -19,8 +19,6 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.0.0-coq-8.16'
-          - 'mathcomp/mathcomp:2.0.0-coq-8.18'
           - 'mathcomp/mathcomp:2.1.0-coq-8.16'
           - 'mathcomp/mathcomp:2.1.0-coq-8.18'
           - 'mathcomp/mathcomp:2.2.0-coq-8.16'
diff --git a/README.md b/README.md
index 96a426f..abf06f1 100644
--- a/README.md
+++ b/README.md
@@ -37,7 +37,7 @@ basic plane topology definitions, and a theory of combinatorial hypermaps.
 - License: [CeCILL-B](LICENSE)
 - Compatible Coq versions: 8.16 or later
 - Additional dependencies:
-  - [MathComp ssreflect 2.0 or later](https://math-comp.github.io)
+  - [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
 - Coq namespace: `fourcolor`
 - Related publication(s):
diff --git a/coq-fourcolor.opam b/coq-fourcolor.opam
index a65cefe..bd63f91 100644
--- a/coq-fourcolor.opam
+++ b/coq-fourcolor.opam
@@ -21,7 +21,7 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
   "coq" {(>= "8.16" & < "8.20~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "2.0.0" & < "2.3~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "2.1.0" & < "2.3~") | (= "dev")}
   "coq-mathcomp-algebra" 
 ]
 
diff --git a/meta.yml b/meta.yml
index 0d3bf59..3413273 100644
--- a/meta.yml
+++ b/meta.yml
@@ -38,10 +38,6 @@ supported_coq_versions:
   opam: '{(>= "8.16" & < "8.20~") | (= "dev")}'
 
 tested_coq_opam_versions:
-- version: '2.0.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '2.0.0-coq-8.18'
-  repo: 'mathcomp/mathcomp'
 - version: '2.1.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
 - version: '2.1.0-coq-8.18'
@@ -64,9 +60,9 @@ ci_cron_schedule: '0 5 * * *'
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "2.0.0" & < "2.3~") | (= "dev")}'
+    version: '{(>= "2.1.0" & < "2.3~") | (= "dev")}'
   description: |-
-    [MathComp ssreflect 2.0 or later](https://math-comp.github.io)
+    [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
   description: |-
diff --git a/theories/realprop.v b/theories/realprop.v
index ed9a2dc..8af8291 100644
--- a/theories/realprop.v
+++ b/theories/realprop.v
@@ -1,7 +1,7 @@
 (* (c) Copyright 2006-2018 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div order.
-From mathcomp Require Import ssralg ssrnum ssrint rat intdiv.
+From mathcomp Require Import ssralg ssrnum ssrint archimedean rat intdiv.
 From Coq Require Import Morphisms Setoid.
 From fourcolor Require Import real realsyntax.
 
@@ -46,7 +46,7 @@ Definition max x y : R := IF x >= y then x else y.
 Definition intR m : R := match m with Posz n => n%:R | Negz n => - n.+1%:R end.
 
 Definition ratR (a : rat) :=
-  if a \is a Qint then intR (numq a) else intR (numq a) / intR (denq a).
+  if a \is a Num.int then intR (numq a) else intR (numq a) / intR (denq a).
 
 Inductive floor_set x : Real.set R :=
   FloorSet m of intR m <= x : floor_set x (intR m).