diff options
Diffstat (limited to 'mathcomp/solvable')
| -rw-r--r-- | mathcomp/solvable/abelian.v | 2 |
1 files changed, 1 insertions, 1 deletions
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). |