diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index c45127d..37ec7a8 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -17,6 +17,7 @@ jobs:
     strategy:
       matrix:
         image:
+          - 'mathcomp/mathcomp:1.12.0-coq-dev'
           - 'mathcomp/mathcomp:1.12.0-coq-8.13'
           - 'mathcomp/mathcomp:1.12.0-coq-8.12'
           - 'mathcomp/mathcomp:1.12.0-coq-8.11'
diff --git a/meta.yml b/meta.yml
index 93fdb99..a44f35b 100644
--- a/meta.yml
+++ b/meta.yml
@@ -83,6 +83,8 @@ dependencies:
     [MathComp](https://math-comp.github.io) 1.11.0 or later
 
 tested_coq_opam_versions:
+- version: '1.12.0-coq-dev'
+  repo: 'mathcomp/mathcomp'
 - version: '1.12.0-coq-8.13'
   repo: 'mathcomp/mathcomp'
 - version: '1.12.0-coq-8.12'
diff --git a/refinements/binnat.v b/refinements/binnat.v
index a6c25e4..22b815c 100644
--- a/refinements/binnat.v
+++ b/refinements/binnat.v
@@ -1,6 +1,6 @@
 (** This file is part of CoqEAL, the Coq Effective Algebra Library.
 (c) Copyright INRIA and University of Gothenburg, see LICENSE *)
-Require Import ZArith.
+Require Import ZArith Lia.
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp.
 From mathcomp Require Import path choice fintype tuple finset ssralg ssrnum bigop ssrint.
@@ -405,13 +405,13 @@ Qed.
 Lemma Nat2Pos_xI m : ((Pos.of_nat m.+1)~1)%positive = Pos.of_nat ((m.+1).*2.+1).
 Proof.
 rewrite -muln2 [RHS]Nat2Pos.inj_succ // Nat2Pos.inj_mul //.
-simpl (Pos.of_nat 2); zify; omega.
+simpl (Pos.of_nat 2); lia.
 Qed.
 
 Lemma Nat2Pos_xO m : ((Pos.of_nat m.+1)~0)%positive = Pos.of_nat ((m.+1).*2).
 Proof.
 rewrite -muln2 Nat2Pos.inj_mul //.
-simpl (Pos.of_nat 2); zify; omega.
+simpl (Pos.of_nat 2); lia.
 Qed.
 
 Lemma pos_of_natE m n : pos_of_nat m n = Pos.of_nat (maxn 1 (m.*2.+1 - n)).
diff --git a/refinements/binrat.v b/refinements/binrat.v
index e89b877..cd16a1a 100644
--- a/refinements/binrat.v
+++ b/refinements/binrat.v
@@ -1,6 +1,6 @@
 (** * A refinement of Mathcomp's rationals [rat] with [bigQ] from Coq standard library. *)
 
-Require Import ZArith QArith.
+Require Import ZArith QArith Lia.
 From Bignums Require Import BigQ.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat order.
 From mathcomp Require Import ssralg ssrnum ssrint rat div.
@@ -215,7 +215,7 @@ Qed.
 
 Lemma Z2int_lt x y : (Z2int x < Z2int y)%R <-> Z.lt x y.
 Proof.
-rewrite -lez_addr1 -[1%R]/(Z2int 1) -Z2int_add Z2int_le; omega.
+rewrite -lez_addr1 -[1%R]/(Z2int 1) -Z2int_add Z2int_le; lia.
 Qed.
 
 Lemma nat_of_pos_Z_to_pos x : nat_of_pos x = `|Z2int (Z.pos x)|%N.