From d762ebb5a8c5191d49a75aa89ec34966de00eb9b Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Thu, 25 Aug 2016 17:44:06 +0200
Subject: better ltngtP

---
 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 e608c4f..45168a0 100644
--- a/mathcomp/solvable/abelian.v
+++ b/mathcomp/solvable/abelian.v
@@ -1745,7 +1745,7 @@ pose cnt_p k := count [pred x : gT | logn p #[x] > k].
 have cnt_b b: \big[dprod/1]_(x <- b) <[x]> = G ->
   count [pred x | #[x] == p ^ k.+1]%N b = cnt_p k b - cnt_p k.+1 b.
 - move/p_bG; elim: b => //= _ b IHb /andP[/p_natP[j ->] /IHb-> {IHb}].
-  rewrite eqn_leq !leq_exp2l ?prime_gt1 // -eqn_leq pfactorK // leqNgt.
+  rewrite eqn_leq !leq_exp2l ?prime_gt1 // -eqn_leq pfactorK //.
   case: ltngtP => // _ {j}; rewrite subSn // add0n; elim: b => //= y b IHb.
   by rewrite leq_add // ltn_neqAle; case: (~~ _).
 by rewrite !cnt_b // /cnt_p !(@count_logn_dprod_cycle _ _ _ G).
-- 
cgit v1.2.3