Improvements

- deprecating `fintype.arg_(min|max)P`
- removing dangling comments connecting min max and meet join
- better compatibility module
- removing broken notations with `\min` and `\max` (no neutral available)
- fixing `incompare` and `incomparel` in order.v
- adding missing elimination lemmas (`(comparable_)?(max|min)E[lg][et]`)
- adding missing `(comparable|real)_arg(min|max)P`
- CHANGELOG update

1 files changed, 3 insertions, 3 deletions

diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v
index 95bc562..3a5caeb 100644
--- a/mathcomp/solvable/abelian.v
+++ b/mathcomp/solvable/abelian.v
@@ -264,7 +264,7 @@ Qed.
 
 Lemma exponent_witness G : nilpotent G -> {x | x \in G & exponent G = #[x]}.
 Proof.
-move=> nilG; have [//=| /= x Gx max_x] := @arg_maxP _ 1 (mem G) order.
+move=> nilG; have [//=| /= x Gx max_x] := @arg_maxnP _ 1 (mem G) order.
 exists x => //; apply/eqP; rewrite eqn_dvd dvdn_exponent // andbT.
 apply/dvdn_biglcmP=> y Gy; apply/dvdn_partP=> //= p.
 rewrite mem_primes => /andP[p_pr _]; have p_gt1: p > 1 := prime_gt1 p_pr.
@@ -726,12 +726,12 @@ Qed.
 
 Lemma grank_min B : 'm(<<B>>) <= #|B|.
 Proof.
-by rewrite /gen_rank; case: arg_minP => [|_ _ -> //]; rewrite genGid.
+by rewrite /gen_rank; case: arg_minnP => [|_ _ -> //]; rewrite genGid.
 Qed.
 
 Lemma grank_witness G : {B | <<B>> = G & #|B| = 'm(G)}.
 Proof.
-rewrite /gen_rank; case: arg_minP => [|B defG _]; first by rewrite genGid.
+rewrite /gen_rank; case: arg_minnP => [|B defG _]; first by rewrite genGid.
 by exists B; first apply/eqP.
 Qed.