Merge pull request #94 from andres-erbsen/less-ZArith_base

adapt to rocq-prover/rocq#19801 (replacing ZArith_base, Zeq_bool)

Author: proux01

BigQ/QMake.v

@@ -181,7 +181,9 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
 
  Theorem spec_eq_bool: forall x y, eq_bool x y = Qeq_bool [x] [y].
  Proof.
- intros. unfold eq_bool. rewrite spec_compare. reflexivity.
+   unfold eq_bool; intros.
+   apply eq_true_iff_eq; rewrite Qeq_bool_iff, spec_compare, Qeq_alt.
+   case Qcompare; intuition congruence.
  Qed.
 
  (** [check_int] : is a reduced fraction [n/d] in fact a integer ? *)

BigZ/BigZ.v

@@ -11,7 +11,7 @@
 From Stdlib Require Import ZProperties ZDivFloor Ring Lia.
 Require Export BigN.
 Require Import ZSig ZSigZAxioms ZMake.
-Import Zpow_def Zdiv.
+Import BinNat Zpow_def Zdiv.
 
 (** * [BigZ] : arbitrary large efficient integers.