diff options
Diffstat (limited to 'mathcomp/solvable')
| -rw-r--r-- | mathcomp/solvable/abelian.v | 4 | ||||
| -rw-r--r-- | mathcomp/solvable/extremal.v | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index 5f93277..95bc562 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -2064,12 +2064,12 @@ apply: eq_bigr => p _; transitivity (p ^ logn p #[x])%N. suffices lti_lnO e: (i < lnO p e _ G) = (e < logn p #[x]). congr (p ^ _)%N; apply/eqP; rewrite eqn_leq andbC; apply/andP; split. by apply/bigmax_leqP=> e; rewrite lti_lnO. - case: (posnP (logn p #[x])) => [-> // | logx_gt0]. + have [-> //|logx_gt0] := posnP (logn p #[x]). have lexpG: (logn p #[x]).-1 < logn p #|G|. by rewrite prednK // dvdn_leq_log ?order_dvdG. by rewrite (@bigmax_sup _ (Ordinal lexpG)) ?(prednK, lti_lnO). rewrite /lnO -(count_logn_dprod_cycle _ _ defG). -case: (ltnP e _) (b_sorted p) => [lt_e_x | le_x_e]. +case: (ltnP e) (b_sorted p) => [lt_e_x | le_x_e]. rewrite -(cat_take_drop i.+1 b) -map_rev rev_cat !map_cat cat_path. case/andP=> _ ordb; rewrite count_cat ((count _ _ =P i.+1) _) ?leq_addr //. rewrite -{2}(size_takel ltib) -all_count. diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v index 36c4d12..42882bc 100644 --- a/mathcomp/solvable/extremal.v +++ b/mathcomp/solvable/extremal.v @@ -2039,7 +2039,7 @@ have [n oG] := p_natP pG; right; rewrite p2 cG /= in oG *. rewrite oG (@leq_exp2l 2 4) //. rewrite /extremal2 /extremal_class oG pfactorKpdiv // in cG. case: andP cG => [[n_gt1 isoG] _ | _]; last first. - by rewrite leq_eqVlt; case: (3 < n); case: eqP => //= <-; do 2?case: ifP. + by case: (ltngtP 3 n) => //= <-; do 2?case: ifP. have [[x y] genG _] := generators_2dihedral n_gt1 isoG. have [_ _ _ [_ _ maxG]] := dihedral2_structure n_gt1 genG isoG. rewrite 2!ltn_neqAle n_gt1 !(eq_sym _ n). |