prettify egcd_coprime_mult

Signed-off-by: Avi Shinnar <[email protected]>
IBM · Dec 11, 2023 · 3c969fe · 3c969fe
1 parent 4c3b373
commit 3c969fe
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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.