diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index bd413c7..cf6066f 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -17,7 +17,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.18'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3
diff --git a/README.md b/README.md
index 1cf9419..29a574f 100644
--- a/README.md
+++ b/README.md
@@ -51,9 +51,9 @@ idealfP
 - License: [MIT License](LICENSE)
 - Compatible Coq versions: 8.17 or later
 - Additional dependencies:
-  - [MathComp ssreflect 1.17 or later](https://math-comp.github.io)
-  - [MathComp algebra 1.17 or later](https://math-comp.github.io)
-  - [MathComp Multinomials 1.6.0 or later](https://github.com/math-comp/multinomials)
+  - [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
+  - [MathComp algebra 2.1 or later](https://math-comp.github.io)
+  - [MathComp Multinomials 2.1.0 or later](https://github.com/math-comp/multinomials)
 - Coq namespace: `grobner`
 - Related publication(s): none
 
diff --git a/coq-grobner.opam b/coq-grobner.opam
index f1e9f21..94937e3 100644
--- a/coq-grobner.opam
+++ b/coq-grobner.opam
@@ -48,9 +48,9 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
   "coq" {(>= "8.17")}
-  "coq-mathcomp-ssreflect" {(>= "1.17.0")}
-  "coq-mathcomp-algebra" {(>= "1.17.0")}
-  "coq-mathcomp-multinomials" {(>= "1.6.0")}
+  "coq-mathcomp-ssreflect" {(>= "2.1.0")}
+  "coq-mathcomp-algebra" {(>= "2.1.0")}
+  "coq-mathcomp-multinomials" {(>= "2.1.0")}
 ]
 
 tags: [
diff --git a/grobner.v b/grobner.v
index 5133c3e..491a554 100644
--- a/grobner.v
+++ b/grobner.v
@@ -1026,7 +1026,7 @@ Proof. by rewrite /spoly subrr if_same. Qed.
 Lemma spoly_sym p q : spoly p q = - (spoly q p).
 Proof.
 rewrite /spoly [_ * p]mulrC; case: (_ == _); first by rewrite oppr0.
-by rewrite opprB [mlcm _ (mlead p)]mlcmC.
+by rewrite [mlcm _ (mlead p)]mlcmC [RHS]opprB.
 Qed.
 
 Lemma ideal_spoly p q : ideal L p -> ideal L q -> ideal L (spoly p q).
diff --git a/meta.yml b/meta.yml
index e1513ef..60562f6 100644
--- a/meta.yml
+++ b/meta.yml
@@ -60,22 +60,22 @@ supported_coq_versions:
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "1.17.0")}'
+    version: '{(>= "2.1.0")}'
   description: |-
-    [MathComp ssreflect 1.17 or later](https://math-comp.github.io)
+    [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{(>= "1.17.0")}'
+    version: '{(>= "2.1.0")}'
   description: |-
-    [MathComp algebra 1.17 or later](https://math-comp.github.io)
+    [MathComp algebra 2.1 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-multinomials
-    version: '{(>= "1.6.0")}'
+    version: '{(>= "2.1.0")}'
   description: |-
-    [MathComp Multinomials 1.6.0 or later](https://github.com/math-comp/multinomials)
+    [MathComp Multinomials 2.1.0 or later](https://github.com/math-comp/multinomials)
 
 tested_coq_opam_versions:
-- version: '1.17.0-coq-8.17'
+- version: '2.1.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
 
 namespace: grobner