diff --git a/BigQ/QMake.v b/BigQ/QMake.v
index cb8cfcb..b1561cf 100644
--- a/BigQ/QMake.v
+++ b/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 ? *)
diff --git a/BigZ/BigZ.v b/BigZ/BigZ.v
index 0582395..6548e3b 100644
--- a/BigZ/BigZ.v
+++ b/BigZ/BigZ.v
@@ -10,7 +10,7 @@
 
 Require Export BigN.
 Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake Ring Lia.
-Import Zpow_def Zdiv.
+Import BinNat Zpow_def Zdiv.
 
 (** * [BigZ] : arbitrary large efficient integers.