diff options
| author | Cyril Cohen | 2016-08-25 17:44:06 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2016-10-24 13:11:31 +0200 |
| commit | d762ebb5a8c5191d49a75aa89ec34966de00eb9b (patch) | |
| tree | 6bc0abd5084ef9db1ff09ae5690bf75df4d63b73 /mathcomp/solvable | |
| parent | fb7060ca71082911284ff6b388c3c45ef07c2723 (diff) | |
better ltngtP
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). |