Extend comparison predicates for nat with minn and maxn

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).