From e9c284b97b76e214f417ccc33907853bc0b8aa8e Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Wed, 29 May 2019 15:37:31 +0300
Subject: incorporate new suggestions by @CohenCyril

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

(limited to 'mathcomp/solvable')

diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v
index dd14013..2e025a2 100644
--- a/mathcomp/solvable/abelian.v
+++ b/mathcomp/solvable/abelian.v
@@ -837,7 +837,7 @@ Qed.
 Lemma rank_gt0 G : ('r(G) > 0) = (G :!=: 1).
 Proof.
 case: (eqsVneq G 1) => [-> |]; first by rewrite rank1.
-case: (trivgVpdiv G) => [-> | [p p_pr]]; first by rewrite eqxx.
+case: (trivgVpdiv G) => [/eqP->// | [p p_pr]].
 case/Cauchy=> // x Gx oxp _; apply: leq_trans (p_rank_le_rank p G).
 have EpGx: <[x]>%G \in 'E_p(G).
   by rewrite inE cycle_subG Gx abelemE // cycle_abelian -oxp exponent_dvdn.
-- 
cgit v1.2.3