diff --git a/src/Coqprime/elliptic/GZnZ.v b/src/Coqprime/elliptic/GZnZ.v
index 695054b..cf60ae0 100644
--- a/src/Coqprime/elliptic/GZnZ.v
+++ b/src/Coqprime/elliptic/GZnZ.v
@@ -25,8 +25,7 @@ intros; subst; auto.
 Qed.
 
 Theorem Zeq_iok: forall x y, x = y -> Zeq_bool x y = true.
-intros x y H; subst.
-unfold Zeq_bool; rewrite Z.compare_refl; auto.
+intros x y H; subst. apply Zeq_is_eq_bool, eq_refl.
 Qed.
 
 Lemma modz: forall x,
diff --git a/src/Coqprime/elliptic/ZEll.v b/src/Coqprime/elliptic/ZEll.v
index fd1f200..6b4fcbe 100644
--- a/src/Coqprime/elliptic/ZEll.v
+++ b/src/Coqprime/elliptic/ZEll.v
@@ -607,11 +607,7 @@ Local Coercion Zpos : positive >-> Z.
   Lemma is_zero_correct: forall x y,
     if (x ?= y) then x = y else x <> y.
   Proof.
-  intros x y; unfold Zeq_bool.
-  case (Zcompare_Eq_iff_eq x y).
-  case Z.compare; auto.
-  intros _ H1 H2; assert (H3:= H1 H2); discriminate.
-  intros _ H1 H2; assert (H3:= H1 H2); discriminate.
+  intros x y. apply Zeq_bool_if.
   Qed.
 
   Lemma inversible_is_not_k0: forall x, [x] -> x :%p  <> 0.