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/solvable/sylow.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/solvable/sylow.v')

diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v
index aed6351..fcbe7e8 100644
--- a/mathcomp/solvable/sylow.v
+++ b/mathcomp/solvable/sylow.v
@@ -267,7 +267,7 @@ Qed.
 
 Lemma card_p2group_abelian P : prime p -> #|P| = (p ^ 2)%N -> abelian P.
 Proof.
-move=> primep oP; have pP: p.-group P by rewrite /pgroup oP pnat_exp pnat_id.
+move=> primep oP; have pP: p.-group P by rewrite /pgroup oP pnatX pnat_id.
 by rewrite (p2group_abelian pP) // oP pfactorK.
 Qed.
 
-- 
cgit v1.2.3