From c6e0d703165b0c60c270672eb542aa8934929bfe Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Fri, 9 Oct 2020 00:21:00 +0900
Subject: Switch from long suffixes to short suffixes

---
 mathcomp/algebra/zmodp.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/algebra/zmodp.v')

diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v
index 015d971..505fda9 100644
--- a/mathcomp/algebra/zmodp.v
+++ b/mathcomp/algebra/zmodp.v
@@ -142,7 +142,7 @@ Proof. by move=> Ux; rewrite /= Zp_mulC Zp_mulVz. Qed.
 Lemma Zp_intro_unit x y : Zp_mul y x = Zp1 -> coprime p x.
 Proof.
 case=> yx1; have:= coprimen1 p.
-by rewrite -coprime_modr -yx1 coprime_modr coprime_mulr; case/andP.
+by rewrite -coprime_modr -yx1 coprime_modr coprimeMr; case/andP.
 Qed.
 
 Lemma Zp_inv_out x : ~~ coprime p x -> Zp_inv x = x.
-- 
cgit v1.2.3