prettify egcd_coprime

Signed-off-by: Avi Shinnar <[email protected]>
IBM · Dec 11, 2023 · 4c3b373 · 4c3b373
1 parent a33cca6
commit 4c3b373
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
@@ -366,8 +366,8 @@ Section chinese.
     (egcdn a b).1 * a = 1 %[mod b].
   Proof.
     intros.
-    destruct (egcdnP b H).
-    rewrite /= e (eqP H0) -modnDm modnMl add0n modn_mod //.
+    case: egcdnP => //= km kn ->.
+    by rewrite (eqP H0) -modnDm modnMl add0n modn_mod.
   Qed.
 
   Lemma egcd_coprime_mult (a b c : nat) :