Extend comparison predicates for nat with minn and maxn

mathcomp/algebra/poly.v

@@ -304,7 +304,7 @@ Canonical opp_poly_unlockable := [unlockable fun opp_poly].
 
 Fact coef_add_poly p q i : (add_poly p q)`_i = p`_i + q`_i.
 Proof.
-rewrite unlock coef_poly; case: leqP => //.
+rewrite unlock coef_poly; case: (ltnP i) => //.
 by rewrite geq_max => /andP[le_p_i le_q_i]; rewrite !nth_default ?add0r.
 Qed.
 
@@ -1257,7 +1257,7 @@ Qed.
 Lemma eq_prim_root_expr i j : (z ^+ i == z ^+ j) = (i == j %[mod n]).
 Proof.
 wlog le_ji: i j / j <= i.
-  move=> IH; case: (leqP j i); last move/ltnW; move/IH=> //.
+  move=> IH; case: (leqP j i) => [|/ltnW] /IH //.
   by rewrite eq_sym (eq_sym (j %% n)%N).
 rewrite -{1}(subnKC le_ji) exprD -prim_expr_mod eqn_mod_dvd //.
 rewrite prim_order_dvd; apply/eqP/eqP=> [|->]; last by rewrite mulr1.

mathcomp/algebra/polydiv.v

@@ -218,7 +218,7 @@ rewrite /rdivp /rmodp /rscalp unlock; case q0 : (q == 0).
 elim: (size p) 0%N 0 {1 3}p (leqnn (size p)) => [|n ihn] k q1 r.
   rewrite leqn0 size_poly_eq0; move/eqP->; rewrite /= size_poly0 /= lt0n.
   by rewrite size_poly_eq0 q0 /= size_poly0 lt0n size_poly_eq0 q0.
-move=> hr /=; case: (@ltnP (size r) _) => //= hsrq; rewrite ihn //.
+move=> hr /=; case: (ltnP (size r)) => //= hsrq; rewrite ihn //.
 apply/leq_sizeP => j hnj; rewrite coefB.
 have sr: 0 < size r.
   by apply: leq_trans hsrq; apply: neq0_lt0n; rewrite size_poly_eq0.
@@ -259,7 +259,7 @@ Qed.
 
 Lemma leq_rmodp m d : size (rmodp m d)  <= size m.
 Proof.
-case: (ltnP (size m) (size d)) => [|h]; first by move/rmodp_small->.
+have [/rmodp_small -> //|h] := ltnP (size m) (size d).
 case d0: (d == 0); first by rewrite (eqP d0) rmodp0.
 by apply: leq_trans h; apply: ltnW; rewrite ltn_rmodp d0.
 Qed.
@@ -1205,10 +1205,9 @@ by rewrite !addnS /= eqn_add2r.
 Qed.
 
 Lemma dvdp_leq p q : q != 0 -> p %| q -> size p <= size q.
-move=> nq0 /modp_eq0P => rpq; case: (ltnP (size p) (size q)).
-   by move/ltnW->.
-rewrite leq_eqVlt; case/orP; first by move/eqP->.
-by move/modp_small; rewrite rpq => h; move: nq0; rewrite h eqxx.
+Proof.
+move=> nq0 /modp_eq0P rqp; rewrite leqNgt.
+apply/contra: nq0 => /modp_small <-; exact/eqP.
 Qed.
 
 Lemma eq_dvdp c quo q p : c != 0 -> c *: p = quo * q -> q %| p.
@@ -1731,12 +1730,12 @@ Proof.
 have [r] := ubnP (minn (size q) (size p)); elim: r => // r IHr in p q *.
 have [-> | nz_p] := eqVneq p 0; first by rewrite gcd0p dvdpp andbT.
 have [-> | nz_q] := eqVneq q 0; first by rewrite gcdp0 dvdpp /=.
-rewrite ltnS gcdpE minnC /minn; case: ltnP => [lt_pq | le_pq] le_qr.
-  suffices /IHr/andP[E1 E2]: minn (size p) (size (q %% p)) < r.
-    by rewrite E2 (dvdp_mod _ E2).
+rewrite ltnS gcdpE; case: leqP => [le_pq | lt_pq] le_qr.
+  suffices /IHr/andP[E1 E2]: minn (size q) (size (p %% q)) < r.
+    by rewrite E2 andbT (dvdp_mod _ E2).
   by rewrite gtn_min orbC (leq_trans _ le_qr) ?ltn_modp.
-suffices /IHr/andP[E1 E2]: minn (size q) (size (p %% q)) < r.
-  by rewrite E2 andbT (dvdp_mod _ E2).
+suffices /IHr/andP[E1 E2]: minn (size p) (size (q %% p)) < r.
+  by rewrite E2 (dvdp_mod _ E2).
 by rewrite gtn_min orbC (leq_trans _ le_qr) ?ltn_modp.
 Qed.
 
@@ -1759,10 +1758,10 @@ apply/idP/andP=> [dv_pmn | []].
 have [r] := ubnP (minn (size n) (size m)); elim: r => // r IHr in m n *.
 have [-> | nz_m] := eqVneq m 0; first by rewrite gcd0p.
 have [-> | nz_n] := eqVneq n 0; first by rewrite gcdp0.
-rewrite gcdpE minnC ltnS /minn; case: ltnP => [lt_mn | le_nm] le_r dv_m dv_n.
-  apply: IHr => //; last by rewrite -(dvdp_mod _ dv_m).
+rewrite gcdpE ltnS; case: leqP => [le_nm | lt_mn] le_r dv_m dv_n.
+  apply: IHr => //; last by rewrite -(dvdp_mod _ dv_n).
   by rewrite gtn_min orbC (leq_trans _ le_r) ?ltn_modp.
-apply: IHr => //; last by rewrite -(dvdp_mod _ dv_n).
+apply: IHr => //; last by rewrite -(dvdp_mod _ dv_m).
 by rewrite gtn_min orbC (leq_trans _ le_r) ?ltn_modp.
 Qed.
 
@@ -1838,11 +1837,9 @@ Proof. by move/dvdp_gcd_idl => h; apply: eqp_trans h; apply: gcdpC. Qed.
 
 Lemma gcdp_exp p k l : gcdp (p ^+ k) (p ^+ l) %= p ^+ minn k l.
 Proof.
-wlog leqmn: k l / k <= l.
-  move=> hwlog; case: (leqP k l); first exact: hwlog.
-  by move/ltnW; rewrite minnC; move/hwlog=> h; apply: eqp_trans h; apply: gcdpC.
-rewrite (minn_idPl leqmn); move/subnK: leqmn<-; rewrite exprD.
-by apply: eqp_trans (gcdp_mull _ _) _; apply: eqpxx.
+suff hwlog k' l': k' <= l' -> gcdp (p ^+ k') (p ^+ l') %= p ^+ k'.
+  by case: leqP => [|/ltnW] /hwlog // /(eqp_trans (gcdpC _ _)).
+by move/subnK => <-; rewrite exprD; exact: gcdp_mull.
 Qed.
 
 Lemma gcdp_eq0 p q : gcdp p q == 0 = (p == 0) && (q == 0).
@@ -1874,18 +1871,16 @@ Lemma eqp_rgcd_gcd p q : rgcdp p q %= gcdp p q.
 Proof.
 move: (leqnn (minn (size p) (size q))); move: {2}(minn (size p) (size q)) => n.
 elim: n p q => [p q|n ihn p q hs].
-  rewrite leqn0 /minn; case: ltnP => _; rewrite size_poly_eq0; move/eqP->.
+  rewrite leqn0; case: ltnP => _; rewrite size_poly_eq0; move/eqP->.
     by rewrite gcd0p rgcd0p eqpxx.
   by rewrite gcdp0 rgcdp0 eqpxx.
 case: (eqVneq p 0) => [-> | pn0]; first by rewrite gcd0p rgcd0p eqpxx.
 case: (eqVneq q 0) => [-> | qn0]; first by rewrite gcdp0 rgcdp0 eqpxx.
-rewrite gcdpE rgcdpE; case: ltnP => sp.
-  have e := (eqp_rmod_mod q p); move: (e); move/(eqp_gcdl p) => h.
-  apply: eqp_trans h; apply: ihn; rewrite (eqp_size e) geq_min.
-  by rewrite -ltnS (leq_trans _ hs) // (minn_idPl (ltnW _)) ?ltn_modp.
-have e := (eqp_rmod_mod p q); move: (e); move/(eqp_gcdl q) => h.
-apply: eqp_trans h; apply: ihn; rewrite (eqp_size e) geq_min.
-by rewrite -ltnS (leq_trans _ hs) // (minn_idPr _) ?ltn_modp.
+rewrite gcdpE rgcdpE; case: ltnP hs => sp hs.
+  have e := eqp_rmod_mod q p; apply: eqp_trans (eqp_gcdl p e); apply: ihn.
+  by rewrite (eqp_size e) geq_min -ltnS (leq_trans _ hs) ?ltn_modp.
+have e := eqp_rmod_mod p q; apply: eqp_trans (eqp_gcdl q e); apply: ihn.
+by rewrite (eqp_size e) geq_min -ltnS (leq_trans _ hs) ?ltn_modp.
 Qed.
 
 Lemma gcdp_modr m n : gcdp m (n %% m) %= gcdp m n.
@@ -2069,9 +2064,9 @@ Qed.
 Lemma egcdpP p q : p != 0 ->  q != 0 -> forall (e := egcdp p q),
   [/\ size e.1 <= size q, size e.2 <= size p & gcdp p q %= e.1 * p + e.2 * q].
 Proof.
-move=> pn0 qn0; rewrite /egcdp; case: (leqP (size q) (size p)) => /= hp.
+move=> pn0 qn0; rewrite /egcdp; case: (leqP (size q) (size p)) => [|/ltnW] hpq.
   by apply: egcdp_recP.
-move/ltnW: hp => hp; case: (egcdp_recP pn0 (leqnn (size p)) hp) => h1 h2 h3.
+case: (egcdp_recP pn0 (leqnn (size p)) hpq) => h1 h2 h3.
 by split => //; rewrite (eqp_ltrans (gcdpC _ _)) addrC.
 Qed.
 

mathcomp/solvable/abelian.v

@@ -2065,12 +2065,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.

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

mathcomp/ssreflect/div.v

@@ -120,7 +120,7 @@ Proof. by case: d => // d; rewrite -[n in n %/ _]muln1 mulKn. Qed.
 
 Lemma divnMl p m d : p > 0 -> p * m %/ (p * d) = m %/ d.
 Proof.
-move=> p_gt0; case: (posnP d) => [-> | d_gt0]; first by rewrite muln0.
+have [->|d_gt0 p_gt0] := posnP d; first by rewrite muln0.
 rewrite [RHS]/divn; case: edivnP; rewrite d_gt0 /= => q r ->{m} lt_rd.
 rewrite mulnDr mulnCA divnMDl; last by rewrite muln_gt0 p_gt0.
 by rewrite addnC divn_small // ltn_pmul2l.
@@ -544,9 +544,9 @@ Lemma edivnS m d : 0 < d -> edivn m.+1 d =
 Proof.
 case: d => [|[|d]] //= _; first by rewrite edivn_def modn1 dvd1n !divn1.
 rewrite -addn1 /dvdn modn_def edivnD//= (@modn_small 1)// (@divn_small 1)//.
-rewrite addn1 addn0 ltnS; case: (ltngtP _ d.+1) => [ | |->].
-- by rewrite addn0 mul0n subn0.
+rewrite addn1 addn0 ltnS; have [||<-] := ltngtP d.+1.
 - by rewrite ltnNge -ltnS ltn_pmod.
+- by rewrite addn0 mul0n subn0.
 - by rewrite addn1 mul1n subnn.
 Qed.
 
@@ -656,10 +656,7 @@ Lemma gcdn_idPr {m n} : reflect (gcdn m n = n) (n %| m).
 Proof. by rewrite gcdnC; apply: gcdn_idPl. Qed.
 
 Lemma expn_min e m n : e ^ minn m n = gcdn (e ^ m) (e ^ n).
-Proof.
-rewrite /minn; case: leqP; [rewrite gcdnC | move/ltnW];
-  by move/(dvdn_exp2l e)/gcdn_idPl.
-Qed.
+Proof. by case: leqP => [|/ltnW] /(dvdn_exp2l e) /gcdn_idPl; rewrite gcdnC. Qed.
 
 Lemma gcdn_modr m n : gcdn m (n %% m) = gcdn m n.
 Proof. by rewrite [in RHS](divn_eq n m) gcdnMDl. Qed.
@@ -863,10 +860,7 @@ Lemma lcmn_idPl {m n} : reflect (lcmn m n = m) (n %| m).
 Proof. by rewrite lcmnC; apply: lcmn_idPr. Qed.
 
 Lemma expn_max e m n : e ^ maxn m n = lcmn (e ^ m) (e ^ n).
-Proof.
-rewrite /maxn; case: leqP; [rewrite lcmnC | move/ltnW];
- by move/(dvdn_exp2l e)/lcmn_idPr.
-Qed.
+Proof. by case: leqP => [|/ltnW] /(dvdn_exp2l e) /lcmn_idPl; rewrite lcmnC. Qed.
 
 (* Coprime factors *)
 

mathcomp/ssreflect/fintype.v

@@ -2037,7 +2037,7 @@ Proof.
 (* match representation is changed to omit these then this proof could reduce *)
 (* to by rewrite /split; case: ltnP; [left | right. rewrite subnKC].          *)
 set lt_i_m := i < m; rewrite /split.
-by case: {-}_ lt_i_m / ltnP; [left | right; rewrite subnKC].
+by case: {-}_ lt_i_m _ _ _ _ / ltnP; [left | right; rewrite subnKC].
 Qed.
 
 Definition unsplit {m n} (jk : 'I_m + 'I_n) :=

mathcomp/ssreflect/order.v

@@ -4074,10 +4074,10 @@ Module NatOrder.
 Section NatOrder.
 
 Lemma minnE x y : minn x y = if (x <= y)%N then x else y.
-Proof. by case: leqP => [/minn_idPl|/ltnW /minn_idPr]. Qed.
+Proof. by have [/minn_idPl|/ltnW /minn_idPr] := leqP. Qed.
 
 Lemma maxnE x y : maxn x y = if (y <= x)%N then x else y.
-Proof. by case: leqP => [/maxn_idPl|/ltnW/maxn_idPr]. Qed.
+Proof. by have [/maxn_idPl|/ltnW/maxn_idPr] := leqP y. Qed.
 
 Lemma ltn_def x y : (x < y)%N = (y != x) && (x <= y)%N.
 Proof. by rewrite ltn_neqAle eq_sym. Qed.

mathcomp/ssreflect/prime.v

@@ -583,7 +583,7 @@ move=> m_gt0 n_gt0; apply/eqP/hasPn=> [mn1 p | no_p_mn].
   rewrite /= !mem_primes m_gt0 n_gt0 /= => /andP[pr_p p_n].
   have:= prime_gt1 pr_p; rewrite pr_p ltnNge -mn1 /=; apply: contra => p_m.
   by rewrite dvdn_leq ?gcdn_gt0 ?m_gt0 // dvdn_gcd ?p_m.
-case: (ltngtP (gcdn m n) 1) => //; first by rewrite ltnNge gcdn_gt0 ?m_gt0.
+apply/eqP; rewrite eqn_leq gcdn_gt0 m_gt0 andbT leqNgt; apply/negP.
 move/pdiv_prime; set p := pdiv _ => pr_p.
 move/implyP: (no_p_mn p); rewrite /= !mem_primes m_gt0 n_gt0 pr_p /=.
 by rewrite !(dvdn_trans (pdiv_dvd _)) // (dvdn_gcdl, dvdn_gcdr).
@@ -956,8 +956,7 @@ Proof. by rewrite ltn_neqAle part_gt0 andbT eq_sym p_part_eq1 negbK. Qed.
 
 Lemma primes_part pi n : primes n`_pi = filter (mem pi) (primes n).
 Proof.
-have ltnT := ltn_trans.
-case: (posnP n) => [-> | n_gt0]; first by rewrite partn0.
+have ltnT := ltn_trans; have [->|n_gt0] := posnP n; first by rewrite partn0.
 apply: (eq_sorted_irr ltnT ltnn); rewrite ?(sorted_primes, sorted_filter) //.
 move=> p; rewrite mem_filter /= !mem_primes n_gt0 part_gt0 /=.
 apply/andP/and3P=> [[p_pr] | [pi_p p_pr dv_p_n]].
@@ -1194,15 +1193,14 @@ Lemma part_pnat_id pi n : pi.-nat n -> n`_pi = n.
 Proof.
 case/andP=> n_gt0 pi_n.
 rewrite -{2}(partnT n_gt0) /partn big_mkcond; apply: eq_bigr=> p _.
-case: (posnP (logn p n)) => [-> |]; first by rewrite if_same.
+have [->|] := posnP (logn p n); first by rewrite if_same.
 by rewrite logn_gt0 => /(allP pi_n)/= ->.
 Qed.
 
 Lemma part_p'nat pi n : pi^'.-nat n -> n`_pi = 1.
 Proof.
 case/andP=> n_gt0 pi'_n; apply: big1_seq => p /andP[pi_p _].
-case: (posnP (logn p n)) => [-> //|].
-by rewrite logn_gt0; move/(allP pi'_n); case/negP.
+by have [-> //|] := posnP (logn p n); rewrite logn_gt0; case/(allP pi'_n)/negP.
 Qed.
 
 Lemma partn_eq1 pi n : n > 0 -> (n`_pi == 1) = pi^'.-nat n.

mathcomp/ssreflect/seq.v

@@ -887,9 +887,7 @@ Lemma all_rev a s : all a (rev s) = all a s.
 Proof. by rewrite !all_count count_rev size_rev. Qed.
 
 Lemma rev_nseq n x : rev (nseq n x) = nseq n x.
-Proof.
-by elim: n => [// | n IHn]; rewrite -{1}(addn1 n) nseq_addn rev_cat IHn.
-Qed.
+Proof. by elim: n => // n IHn; rewrite -{1}(addn1 n) nseq_addn rev_cat IHn. Qed.
 
 End Sequences.
 
@@ -1736,14 +1734,14 @@ Proof. exact (can_inj rotrK). Qed.
 Lemma take_rev s : take n0 (rev s) = rev (drop (size s - n0) s).
 Proof.
 set m := _ - n0; rewrite -[s in LHS](cat_take_drop m) rev_cat take_cat.
-rewrite size_rev size_drop -minnE minnC ltnNge geq_minl [in take m s]/m /minn.
+rewrite size_rev size_drop -minnE minnC leq_min ltnn /m.
 by have [_|/eqnP->] := ltnP; rewrite ?subnn take0 cats0.
 Qed.
 
 Lemma drop_rev s : drop n0 (rev s) = rev (take (size s - n0) s).
 Proof.
 set m := _ - n0; rewrite -[s in LHS](cat_take_drop m) rev_cat drop_cat.
-rewrite size_rev size_drop -minnE minnC ltnNge geq_minl /= /m /minn.
+rewrite size_rev size_drop -minnE minnC leq_min ltnn /m.
 by have [_|/eqnP->] := ltnP; rewrite ?take0 // subnn drop0.
 Qed.
 
@@ -2411,29 +2409,27 @@ Proof.
 by move/subnKC <-; rewrite addSnnS iota_add nth_cat size_iota ltnn subnn.
 Qed.
 
-Lemma mem_iota m n i : (i \in iota m n) = (m <= i) && (i < m + n).
+Lemma mem_iota m n i : (i \in iota m n) = (m <= i < m + n).
 Proof.
 elim: n m => [|n IHn] /= m; first by rewrite addn0 ltnNge andbN.
-rewrite -addSnnS leq_eqVlt in_cons eq_sym.
-by case: eqP => [->|_]; [rewrite leq_addr | apply: IHn].
+by rewrite in_cons IHn addnS ltnS; case: ltngtP => // ->; rewrite leq_addr.
 Qed.
 
 Lemma iota_uniq m n : uniq (iota m n).
 Proof. by elim: n m => //= n IHn m; rewrite mem_iota ltnn /=. Qed.
 
 Lemma take_iota k m n : take k (iota m n) = iota m (minn k n).
 Proof.
-rewrite /minn; case: ltnP => [lt_k_n|le_n_k].
-  by elim: k n lt_k_n m => [|k IHk] [|n]//= H m; rewrite IHk.
+have [lt_k_n|le_n_k] := ltnP.
+  by elim: k n lt_k_n m => [|k IHk] [|n] //= H m; rewrite IHk.
 by apply: take_oversize; rewrite size_iota.
 Qed.
 
 Lemma drop_iota k m n : drop k (iota m n) = iota (m + k) (n - k).
 Proof.
-by elim: k m n => [|k IHk] m [|n]//=; rewrite ?addn0// IHk addSn addnS subSS.
+by elim: k m n => [|k IHk] m [|n] //=; rewrite ?addn0 // IHk addnS subSS.
 Qed.
 
-
 (* Making a sequence of a specific length, using indexes to compute items. *)
 
 Section MakeSeq.