Require Znumtheory before using it

.github/workflows/docker-action.yml

@@ -28,18 +28,19 @@ jobs:
           - 'mathcomp/mathcomp:2.2.0-coq-8.18'
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
           - 'mathcomp/mathcomp:2.2.0-coq-8.20'
-          - 'mathcomp/mathcomp:2.2.0-coq-dev'
           - 'mathcomp/mathcomp:2.3.0-coq-8.18'
           - 'mathcomp/mathcomp:2.3.0-coq-8.19'
           - 'mathcomp/mathcomp:2.3.0-coq-8.20'
-          - 'mathcomp/mathcomp:2.3.0-coq-dev'
-          - 'mathcomp/mathcomp-dev:coq-8.18'
-          - 'mathcomp/mathcomp-dev:coq-8.19'
+          - 'mathcomp/mathcomp:2.4.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.4.0-coq-8.20'
+          - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0'
+          - 'mathcomp/mathcomp:2.4.0-rocq-prover-dev'
           - 'mathcomp/mathcomp-dev:coq-8.20'
-          - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp-dev:rocq-prover-9.0'
+          - 'mathcomp/mathcomp-dev:rocq-prover-dev'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-mathcomp-zify.opam'

meta.yml

@@ -53,23 +53,25 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
-- version: '2.2.0-coq-dev'
-  repo: 'mathcomp/mathcomp'
 - version: '2.3.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
 - version: '2.3.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
 - version: '2.3.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
-- version: '2.3.0-coq-dev'
+- version: '2.4.0-coq-8.19'
+  repo: 'mathcomp/mathcomp'
+- version: '2.4.0-coq-8.20'
+  repo: 'mathcomp/mathcomp'
+- version: '2.4.0-rocq-prover-9.0'
+  repo: 'mathcomp/mathcomp'
+- version: '2.4.0-rocq-prover-dev'
   repo: 'mathcomp/mathcomp'
-- version: 'coq-8.18'
-  repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.19'
-  repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.20'
   repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-dev'
+- version: 'rocq-prover-9.0'
+  repo: 'mathcomp/mathcomp-dev'
+- version: 'rocq-prover-dev'
   repo: 'mathcomp/mathcomp-dev'
 
 dependencies:

theories/zify_ssreflect.v

@@ -1,8 +1,9 @@
 From Coq Require Import ZArith ZifyClasses ZifyInst ZifyBool.
 From Coq Require Export Lia.
+From Coq Require Znumtheory.
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
 From mathcomp Require Import div choice fintype tuple finfun bigop finset prime.
 From mathcomp Require Import order binomial.
 
 Set Implicit Arguments.
@@ -154,7 +155,7 @@
 Add Zify BinOp Op_eq_op_nat.
 
 #[global]
 Instance Op_addn_rec : BinOp addn_rec := Op_plus.
 Add Zify BinOp Op_addn_rec.
 
 #[global]
@@ -167,7 +168,7 @@
 Add Zify BinOp Op_addn_trec.
 
 #[global]
 Instance Op_subn_rec : BinOp subn_rec := Op_sub.
 Add Zify BinOp Op_subn_rec.
 
 #[global]
@@ -175,7 +176,7 @@
 Add Zify BinOp Op_subn.
 
 #[global]
 Instance Op_muln_rec : BinOp muln_rec := Op_mul.
 Add Zify BinOp Op_muln_rec.
 
 #[global]
@@ -236,7 +237,7 @@
 Proof. rewrite -Zpower_nat_Z; elim: m => //= m <-; rewrite expnS; lia. Qed.
 
 #[global]
 Instance Op_expn_rec : BinOp expn_rec :=
   { TBOp := Z.pow; TBOpInj := Op_expn_subproof }.
 Add Zify BinOp Op_expn_rec.
 
@@ -387,7 +388,7 @@
 Fact modZ_ge0 m d : d <> 0%Z -> (0 <= modZ m d)%Z.
 Proof.
 by move: d m => [] // d [] // m _; rewrite /modZ /divZ [Z.abs_nat _]/=;
   move: (leq_trunc_div (Pos.to_nat m) (Pos.to_nat d));
   move: (@ltn_ceil (Pos.to_nat m).-1 (Pos.to_nat d)); lia.
 Qed.