diff --git a/coq/FHE/zp_prim_root.v b/coq/FHE/zp_prim_root.v
index f7841b3c..24e60ac8 100644
--- a/coq/FHE/zp_prim_root.v
+++ b/coq/FHE/zp_prim_root.v
@@ -379,8 +379,8 @@ Section chinese.
     intros.
     rewrite -mulnA -modnMmr egcd_coprime //.
     rewrite modnS mod0n dvdn1.
-    case (boolP (b == 1)); intros HH; move /eqP in HH.
-    - by rewrite HH muln0 !modn1.
+    case: eqVneq => [-> |].
+    - by rewrite muln0 !modn1.
     - by rewrite muln1.
   Qed.