From 85039b4c536a67ce936c079f519a9a8b6c33f1d6 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Fri, 15 Nov 2019 19:46:20 +0900
Subject: Extend comparison predicates for nat with minn and maxn

---
 mathcomp/algebra/polydiv.v   | 105 ++++++++++--------------------
 mathcomp/solvable/abelian.v  |   4 +-
 mathcomp/solvable/extremal.v |   2 +-
 mathcomp/ssreflect/div.v     |  16 ++---
 mathcomp/ssreflect/fintype.v |   2 +-
 mathcomp/ssreflect/order.v   |   4 +-
 mathcomp/ssreflect/prime.v   |  10 ++-
 mathcomp/ssreflect/seq.v     |  20 +++---
 mathcomp/ssreflect/ssrnat.v  | 152 ++++++++++++++++++++++++++++---------------
 9 files changed, 158 insertions(+), 157 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v
index afd0c6c..a7d3b1e 100644
--- a/mathcomp/algebra/polydiv.v
+++ b/mathcomp/algebra/polydiv.v
@@ -241,7 +241,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).
 have [->|d0] := eqVneq d 0; first by rewrite rmodp0.
 by apply: leq_trans h; apply: ltnW; rewrite ltn_rmodp.
 Qed.
@@ -1106,7 +1106,7 @@ Qed.
 Lemma dvdp_leq p q : q != 0 -> p %| q -> size p <= size q.
 Proof.
 move=> nq0 /modp_eq0P.
-by case: ltngtP => // /modp_small -> /eqP; rewrite (negPf nq0).
+by case: leqP => // /modp_small -> /eqP; rewrite (negPf nq0).
 Qed.
 
 Lemma eq_dvdp c quo q p : c != 0 -> c *: p = quo * q -> q %| p.
@@ -1359,24 +1359,16 @@ by rewrite /eqp (dvdp_trans Dp) // (dvdp_trans qD).
 Qed.
 
 Lemma eqp_ltrans : left_transitive (@eqp R).
-Proof.
-by move=> p q r pq; apply/idP/idP; apply: eqp_trans; rewrite // eqp_sym.
-Qed.
+Proof. exact: sym_left_transitive eqp_sym eqp_trans. Qed.
 
 Lemma eqp_rtrans : right_transitive (@eqp R).
-Proof. by move=> x y xy z; rewrite eqp_sym (eqp_ltrans xy) eqp_sym. Qed.
+Proof. exact: sym_right_transitive eqp_sym eqp_trans. Qed.
 
 Lemma eqp0 p : (p %= 0) = (p == 0).
-Proof.
-have [->|Ep] := eqVneq; first by rewrite ?eqpxx.
-by apply/negP => /andP [_]; rewrite /dvdp modp0 (negPf Ep).
-Qed.
+Proof. by apply/idP/eqP => [/andP [_ /dvd0pP] | -> //]. Qed.
 
 Lemma eqp01 : 0 %= (1 : {poly R}) = false.
-Proof.
-case: eqpP => // -[[c1 c2]] /andP [c1n0 c2n0] /= /esym /eqP.
-by rewrite scaler0 alg_polyC polyC_eq0 (negPf c2n0).
-Qed.
+Proof. by rewrite eqp_sym eqp0 oner_eq0. Qed.
 
 Lemma eqp_scale p c : c != 0 -> c *: p %= p.
 Proof.
@@ -1597,12 +1589,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.
 
@@ -1623,10 +1615,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.
 
@@ -1702,11 +1694,8 @@ Proof. by move/dvdp_gcd_idl; exact/eqp_trans/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; apply/eqp_trans/gcdpC.
-rewrite (minn_idPl leqmn); move/subnK: leqmn<-; rewrite exprD.
-by apply: eqp_trans (gcdp_mull _ _) _; apply: eqpxx.
+case: leqP => [|/ltnW] /subnK <-; rewrite exprD; first exact: gcdp_mull.
+exact/(eqp_trans (gcdpC _ _))/gcdp_mull.
 Qed.
 
 Lemma gcdp_eq0 p q : gcdp p q == 0 = (p == 0) && (q == 0).
@@ -1730,40 +1719,33 @@ by rewrite -(eqp_dvdr _ eqr) dvdp_gcdl (eqp_dvdr _ eqr) dvdp_gcdl.
 Qed.
 
 Lemma eqp_gcd p1 p2 q1 q2 : p1 %= p2 -> q1 %= q2 -> gcdp p1 q1 %= gcdp p2 q2.
-Proof.
-move=> e1 e2.
-by apply: eqp_trans (eqp_gcdr _ e2); apply: eqp_trans (eqp_gcdl _ e1).
-Qed.
+Proof. move=> e1 e2; exact: eqp_trans (eqp_gcdr _ e2) (eqp_gcdl _ e1). Qed.
 
 Lemma eqp_rgcd_gcd p q : rgcdp p q %= gcdp p q.
 Proof.
 move: {2}(minn (size p) (size q)) (leqnn (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.
 have [-> | pn0] := eqVneq p 0; first by rewrite gcd0p rgcd0p eqpxx.
 have [-> | qn0] := eqVneq q 0; first by rewrite gcdp0 rgcdp0 eqpxx.
-rewrite gcdpE rgcdpE; case: ltnP => sp.
+rewrite gcdpE rgcdpE; case: ltnP hs => sp hs.
   have e := eqp_rmod_mod q p; apply/eqp_trans/ihn: (eqp_gcdl p e).
-  rewrite (eqp_size e) geq_min -ltnS (leq_trans _ hs) //.
-  by rewrite (minn_idPl (ltnW _)) ?ltn_modp.
+  by rewrite (eqp_size e) geq_min -ltnS (leq_trans _ hs) ?ltn_modp.
 have e := eqp_rmod_mod p q; apply/eqp_trans/ihn: (eqp_gcdl q e).
-rewrite (eqp_size e) geq_min -ltnS (leq_trans _ hs) //.
-by rewrite (minn_idPr _) ?ltn_modp.
+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.
+Lemma gcdp_modl m n : gcdp (m %% n) n %= gcdp m n.
 Proof.
-have [-> | mn0] := eqVneq m 0; first by rewrite modp0 eqpxx.
-have : (lead_coef m) ^+ (scalp n m) != 0 by rewrite expf_neq0 // lead_coef_eq0.
-move/(gcdp_scaler m n); apply/eqp_trans.
-by rewrite divp_eq eqp_sym gcdp_addl_mul.
+have [/modp_small -> // | lenm] := ltnP (size m) (size n).
+by rewrite (gcdpE m n) ltnNge lenm.
 Qed.
 
-Lemma gcdp_modl m n : gcdp (m %% n) n %= gcdp m n.
+Lemma gcdp_modr m n : gcdp m (n %% m) %= gcdp m n.
 Proof.
-apply: eqp_trans (gcdpC _ _); apply: eqp_trans (gcdp_modr _ _); exact: gcdpC.
+apply: eqp_trans (gcdpC _ _); apply: eqp_trans (gcdp_modl _ _); exact: gcdpC.
 Qed.
 
 Lemma gcdp_def d m n :
@@ -2798,10 +2780,7 @@ by rewrite modp_scaler ?eqpxx // mulf_eq0 negb_or invr_eq0 c1n0.
 Qed.
 
 Lemma eqp_mod p1 p2 q1 q2 : p1 %= p2 -> q1 %= q2 -> p1 %% q1 %= p2 %% q2.
-Proof.
-move=> e1 e2; apply: eqp_trans (eqp_modpr _ e2).
-by apply: eqp_trans (eqp_modpl _ e1); apply: eqpxx.
-Qed.
+Proof. move=> e1 e2; exact: eqp_trans (eqp_modpl _ e1) (eqp_modpr _ e2). Qed.
 
 Lemma eqp_divr (d m n : {poly F}) : m %= n -> (d %/ m) %= (d %/ n).
 Proof.
@@ -2811,10 +2790,7 @@ by rewrite divp_scaler ?eqp_scale // ?invr_eq0 mulf_eq0 negb_or invr_eq0 c1n0.
 Qed.
 
 Lemma eqp_div p1 p2 q1 q2 : p1 %= p2 -> q1 %= q2 -> p1 %/ q1 %= p2 %/ q2.
-Proof.
-move=> e1 e2; apply: eqp_trans (eqp_divr _ e2).
-by apply: eqp_trans (eqp_divl _ e1); apply: eqpxx.
-Qed.
+Proof. move=> e1 e2; exact: eqp_trans (eqp_divl _ e1) (eqp_divr _ e2). Qed.
 
 Lemma eqp_gdcor p q r : q %= r -> gdcop p q %= gdcop p r.
 Proof.
@@ -2847,42 +2823,33 @@ case: ifP=> // _; apply: ihn => //; apply: eqp_trans (eqp_rdiv_div _ _) _.
 by apply: eqp_div => //; apply: eqp_trans (eqp_rgcd_gcd _ _) _; apply: eqp_gcd.
 Qed.
 
-Lemma modp_opp p q : (- p) %% q = - (p %% q).
-Proof.
-have [-> | qn0] := eqVneq q 0; first by rewrite !modp0.
-by apply: IdomainUnit.modp_opp; rewrite unitfE lead_coef_eq0.
-Qed.
-
-Lemma divp_opp p q : (- p) %/ q = - (p %/ q).
-Proof.
-have [-> | qn0] := eqVneq q 0; first by rewrite !divp0 oppr0.
-by apply: IdomainUnit.divp_opp; rewrite unitfE lead_coef_eq0.
-Qed.
-
 Lemma modp_add d p q : (p + q) %% d = p %% d + q %% d.
 Proof.
 have [-> | dn0] := eqVneq d 0; first by rewrite !modp0.
 by apply: IdomainUnit.modp_add; rewrite unitfE lead_coef_eq0.
 Qed.
 
-Lemma modNp p q : (- p) %% q = - (p %% q).
+Lemma modp_opp p q : (- p) %% q = - (p %% q).
 Proof. by apply/eqP; rewrite -addr_eq0 -modp_add addNr mod0p. Qed.
 
+Lemma modNp p q : (- p) %% q = - (p %% q). Proof. exact: modp_opp. Qed.
+
 Lemma divp_add d p q : (p + q) %/ d = p %/ d + q %/ d.
 Proof.
 have [-> | dn0] := eqVneq d 0; first by rewrite !divp0 addr0.
 by apply: IdomainUnit.divp_add; rewrite unitfE lead_coef_eq0.
 Qed.
 
-Lemma divp_addl_mul_small d q r :
-  size r < size d -> (q * d + r) %/ d = q.
+Lemma divp_opp p q : (- p) %/ q = - (p %/ q).
+Proof. by apply/eqP; rewrite -addr_eq0 -divp_add addNr div0p. Qed.
+
+Lemma divp_addl_mul_small d q r : size r < size d -> (q * d + r) %/ d = q.
 Proof.
 move=> srd; rewrite divp_add (divp_small srd) addr0 mulpK //.
 by rewrite -size_poly_gt0; apply: leq_trans srd.
 Qed.
 
-Lemma modp_addl_mul_small d q r :
-  size r < size d -> (q * d + r) %% d = r.
+Lemma modp_addl_mul_small d q r : size r < size d -> (q * d + r) %% d = r.
 Proof. by move=> srd; rewrite modp_add modp_mull add0r modp_small. Qed.
 
 Lemma divp_addl_mul d q r : d != 0 -> (q * d + r) %/ d = q + r %/ d.
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).
diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index 06a6ff1..b366055 100644
--- a/mathcomp/ssreflect/div.v
+++ b/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.
+move=> p_gt0; have [->|d_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 *)
 
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 14d623f..6c27b73 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/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) :=
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index 5c8f251..b261072 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -4556,10 +4556,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 case: 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 case: leqP. Qed.
 
 Lemma ltn_def x y : (x < y)%N = (y != x) && (x <= y)%N.
 Proof. by rewrite ltn_neqAle eq_sym. Qed.
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index d8f5939..b71f5e7 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/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.
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 5b9d047..65cc122 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/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,11 +2409,10 @@ 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).
@@ -2423,17 +2420,16 @@ 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.
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index bccb968..7de4ad4 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -474,47 +474,6 @@ Arguments ltP {m n}.
 Lemma lt_irrelevance m n lt_mn1 lt_mn2 : lt_mn1 = lt_mn2 :> (m < n)%coq_nat.
 Proof. exact: (@le_irrelevance m.+1). Qed.
 
-(* Comparison predicates. *)
-
-Variant leq_xor_gtn m n : bool -> bool -> Set :=
-  | LeqNotGtn of m <= n : leq_xor_gtn m n true false
-  | GtnNotLeq of n < m  : leq_xor_gtn m n false true.
-
-Lemma leqP m n : leq_xor_gtn m n (m <= n) (n < m).
-Proof.
-by rewrite ltnNge; case le_mn: (m <= n); constructor; rewrite // ltnNge le_mn.
-Qed.
-
-Variant ltn_xor_geq m n : bool -> bool -> Set :=
-  | LtnNotGeq of m < n  : ltn_xor_geq m n false true
-  | GeqNotLtn of n <= m : ltn_xor_geq m n true false.
-
-Lemma ltnP m n : ltn_xor_geq m n (n <= m) (m < n).
-Proof. by case: leqP; constructor. Qed.
-
-Variant eqn0_xor_gt0 n : bool -> bool -> Set :=
-  | Eq0NotPos of n = 0 : eqn0_xor_gt0 n true false
-  | PosNotEq0 of n > 0 : eqn0_xor_gt0 n false true.
-
-Lemma posnP n : eqn0_xor_gt0 n (n == 0) (0 < n).
-Proof. by case: n; constructor. Qed.
-
-Variant compare_nat m n :
-   bool -> bool -> bool -> bool -> bool -> bool -> Set :=
-  | CompareNatLt of m < n : compare_nat m n false false false true false true
-  | CompareNatGt of m > n : compare_nat m n false false true false true false
-  | CompareNatEq of m = n : compare_nat m n true true true true false false.
-
-Lemma ltngtP m n : compare_nat m n (n == m) (m == n) (n <= m)
-                                   (m <= n) (n < m) (m < n).
-Proof.
-rewrite !ltn_neqAle [_ == n]eq_sym; case: ltnP => [nm|].
-  by rewrite ltnW // gtn_eqF //; constructor.
-rewrite leq_eqVlt; case: ltnP; rewrite ?(orbT, orbF) => //= lt_mn eq_nm.
-  by rewrite ltn_eqF //; constructor.
-by rewrite eq_nm; constructor; apply/esym/eqP.
-Qed.
-
 (* Monotonicity lemmas *)
 
 Lemma leq_add2l p m n : (p + m <= p + n) = (m <= n).
@@ -656,13 +615,6 @@ Proof. by move=> np pm; rewrite !leq_subRL // addnC. Qed.
 Lemma ltn_subCl m n p : n <= m -> p <= m -> (m - n < p) = (m - p < n).
 Proof. by move=> nm pm; rewrite !ltn_subLR // addnC. Qed.
 
-(* Eliminating the idiom for structurally decreasing compare and subtract. *)
-Lemma subn_if_gt T m n F (E : T) :
-  (if m.+1 - n is m'.+1 then F m' else E) = (if n <= m then F (m - n) else E).
-Proof.
-by case: leqP => [le_nm | /eqnP-> //]; rewrite -{1}(subnK le_nm) -addSn addnK.
-Qed.
-
 (* Max and min. *)
 
 Definition maxn m n := if m < n then n else m.
@@ -673,10 +625,13 @@ Lemma max0n : left_id 0 maxn.  Proof. by case. Qed.
 Lemma maxn0 : right_id 0 maxn. Proof. by []. Qed.
 
 Lemma maxnC : commutative maxn.
-Proof. by move=> m n; rewrite /maxn; case ltngtP. Qed.
+Proof. by rewrite /maxn; elim=> [|m ih] [] // n; rewrite !ltnS -!fun_if ih. Qed.
 
 Lemma maxnE m n : maxn m n = m + (n - m).
-Proof. by rewrite /maxn addnC; case: leqP => [/eqnP->|/ltnW/subnK]. Qed.
+Proof.
+rewrite /maxn; elim: m n => [|m ih] [|n]; rewrite ?addn0 //.
+by rewrite ltnS subSS addSn -ih; case: leq.
+Qed.
 
 Lemma maxnAC : right_commutative maxn.
 Proof. by move=> m n p; rewrite !maxnE -!addnA !subnDA -!maxnE maxnC. Qed.
@@ -727,10 +682,10 @@ Lemma min0n : left_zero 0 minn. Proof. by case. Qed.
 Lemma minn0 : right_zero 0 minn. Proof. by []. Qed.
 
 Lemma minnC : commutative minn.
-Proof. by move=> m n; rewrite /minn; case ltngtP. Qed.
+Proof. by rewrite /minn; elim=> [|m ih] [] // n; rewrite !ltnS -!fun_if ih. Qed.
 
 Lemma addn_min_max m n : minn m n + maxn m n = m + n.
-Proof. by rewrite /minn /maxn; case: ltngtP => // [_|->] //; apply: addnC. Qed.
+Proof. by rewrite /minn /maxn; case: (m < n) => //; exact: addnC. Qed.
 
 Lemma minnE m n : minn m n = m - (m - n).
 Proof. by rewrite -(subnDl n) -maxnE -addn_min_max addnK minnC. Qed.
@@ -765,7 +720,8 @@ Lemma leq_min m n1 n2 : (m <= minn n1 n2) = (m <= n1) && (m <= n2).
 Proof.
 wlog le_n21: n1 n2 / n2 <= n1.
   by case/orP: (leq_total n2 n1) => ?; last rewrite minnC andbC; auto.
-by rewrite /minn ltnNge le_n21 /= andbC; case: leqP => // /leq_trans->.
+rewrite /minn ltnNge le_n21 /=; case le_m_n1: (m <= n1) => //=.
+apply/contraFF: le_m_n1 => /leq_trans; exact.
 Qed.
 
 Lemma gtn_min m n1 n2 : (m > minn n1 n2) = (m > n1) || (m > n2).
@@ -820,6 +776,61 @@ Qed.
 Lemma minn_maxr : right_distributive minn maxn.
 Proof. by move=> m n1 n2; rewrite !(minnC m) minn_maxl. Qed.
 
+(* Comparison predicates. *)
+
+Variant leq_xor_gtn m n : nat -> nat -> nat -> nat -> bool -> bool -> Set :=
+  | LeqNotGtn of m <= n : leq_xor_gtn m n m m n n true false
+  | GtnNotLeq of n < m  : leq_xor_gtn m n n n m m false true.
+
+Lemma leqP m n : leq_xor_gtn m n (minn n m) (minn m n) (maxn n m) (maxn m n)
+                                 (m <= n) (n < m).
+Proof.
+rewrite (minnC m) /minn (maxnC m) /maxn ltnNge.
+by case le_mn: (m <= n); constructor; rewrite //= ltnNge le_mn.
+Qed.
+
+Variant ltn_xor_geq m n : nat -> nat -> nat -> nat -> bool -> bool -> Set :=
+  | LtnNotGeq of m < n  : ltn_xor_geq m n m m n n false true
+  | GeqNotLtn of n <= m : ltn_xor_geq m n n n m m true false.
+
+Lemma ltnP m n : ltn_xor_geq m n (minn n m) (minn m n) (maxn n m) (maxn m n)
+                                 (n <= m) (m < n).
+Proof. by case: leqP; constructor. Qed.
+
+Variant eqn0_xor_gt0 n : bool -> bool -> Set :=
+  | Eq0NotPos of n = 0 : eqn0_xor_gt0 n true false
+  | PosNotEq0 of n > 0 : eqn0_xor_gt0 n false true.
+
+Lemma posnP n : eqn0_xor_gt0 n (n == 0) (0 < n).
+Proof. by case: n; constructor. Qed.
+
+Variant compare_nat m n : nat -> nat -> nat -> nat ->
+                          bool -> bool -> bool -> bool -> bool -> bool -> Set :=
+  | CompareNatLt of m < n :
+      compare_nat m n m m n n false false false true false true
+  | CompareNatGt of m > n :
+      compare_nat m n n n m m false false true false true false
+  | CompareNatEq of m = n :
+      compare_nat m n m m m m true true true true false false.
+
+Lemma ltngtP m n :
+  compare_nat m n (minn n m) (minn m n) (maxn n m) (maxn m n)
+                  (n == m) (m == n) (n <= m) (m <= n) (n < m) (m < n).
+Proof.
+rewrite !ltn_neqAle [_ == n]eq_sym; have [mn|] := ltnP m n.
+  by rewrite ltnW // gtn_eqF //; constructor.
+rewrite leq_eqVlt; case: ltnP; rewrite ?(orbT, orbF) => //= lt_nm eq_nm.
+  by rewrite ltn_eqF //; constructor.
+by rewrite eq_nm (eqP eq_nm); constructor.
+Qed.
+
+(* Eliminating the idiom for structurally decreasing compare and subtract. *)
+Lemma subn_if_gt T m n F (E : T) :
+  (if m.+1 - n is m'.+1 then F m' else E) = (if n <= m then F (m - n) else E).
+Proof.
+by have [le_nm|/eqnP-> //] := leqP; rewrite -{1}(subnK le_nm) -addSn addnK.
+Qed.
+
 (* Getting a concrete value from an abstract existence proof. *)
 
 Section ExMinn.
@@ -1872,3 +1883,38 @@ Lemma ltngtP m n : compare_nat m n (m <= n) (n <= m) (m < n)
 Proof. by case: ltngtP; constructor. Qed.
 
 End mc_1_9.
+
+Module mc_1_10.
+
+Variant leq_xor_gtn m n : bool -> bool -> Set :=
+  | LeqNotGtn of m <= n : leq_xor_gtn m n true false
+  | GtnNotLeq of n < m  : leq_xor_gtn m n false true.
+
+Lemma leqP m n : leq_xor_gtn m n (m <= n) (n < m).
+Proof. by case: leqP; constructor. Qed.
+
+Variant ltn_xor_geq m n : bool -> bool -> Set :=
+  | LtnNotGeq of m < n  : ltn_xor_geq m n false true
+  | GeqNotLtn of n <= m : ltn_xor_geq m n true false.
+
+Lemma ltnP m n : ltn_xor_geq m n (n <= m) (m < n).
+Proof. by case: ltnP; constructor. Qed.
+
+Variant eqn0_xor_gt0 n : bool -> bool -> Set :=
+  | Eq0NotPos of n = 0 : eqn0_xor_gt0 n true false
+  | PosNotEq0 of n > 0 : eqn0_xor_gt0 n false true.
+
+Lemma posnP n : eqn0_xor_gt0 n (n == 0) (0 < n).
+Proof. by case: n; constructor. Qed.
+
+Variant compare_nat m n :
+   bool -> bool -> bool -> bool -> bool -> bool -> Set :=
+  | CompareNatLt of m < n : compare_nat m n false false false true false true
+  | CompareNatGt of m > n : compare_nat m n false false true false true false
+  | CompareNatEq of m = n : compare_nat m n true true true true false false.
+
+Lemma ltngtP m n : compare_nat m n (n == m) (m == n) (n <= m)
+                                   (m <= n) (n < m) (m < n).
+Proof. by case: ltngtP; constructor. Qed.
+
+End mc_1_10.
-- 
cgit v1.2.3


From bdb23c100648a7e1b055d90a76eedbff9eef12f4 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Thu, 9 Jan 2020 18:56:55 +0900
Subject: Reorder arguments of comparison predicates in order.v as they should

---
 mathcomp/algebra/ssrnum.v  | 10 +++-------
 mathcomp/ssreflect/order.v | 44 ++++++++++++++++++++++----------------------
 2 files changed, 25 insertions(+), 29 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index f9b4cb0..0ad7f20 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -3823,17 +3823,13 @@ Lemma oppr_min : {morph -%R : x y / min x y >-> max x y : R}.
 Proof. by move=> x y; rewrite -[max _ _]opprK oppr_max !opprK. Qed.
 
 Lemma addr_minl : @left_distributive R R +%R min.
-Proof.
-by move=> x y z; case: leP; case: leP => //; rewrite lter_add2; case: leP.
-Qed.
+Proof. by move=> x y z; case: (leP (_ + _)); rewrite lter_add2; case: leP. Qed.
 
 Lemma addr_minr : @right_distributive R R +%R min.
 Proof. by move=> x y z; rewrite !(addrC x) addr_minl. Qed.
 
 Lemma addr_maxl : @left_distributive R R +%R max.
-Proof.
-by move=> x y z; case: leP; case: leP => //; rewrite lter_add2; case: leP.
-Qed.
+Proof. by move=> x y z; case: (leP (_ + _)); rewrite lter_add2; case: leP. Qed.
 
 Lemma addr_maxr : @right_distributive R R +%R max.
 Proof. by move=> x y z; rewrite !(addrC x) addr_maxl. Qed.
@@ -3841,7 +3837,7 @@ Proof. by move=> x y z; rewrite !(addrC x) addr_maxl. Qed.
 Lemma minr_pmulr x y z : 0 <= x -> x * min y z = min (x * y) (x * z).
 Proof.
 case: sgrP=> // hx _; first by rewrite hx !mul0r meetxx.
-by case: leP; case: leP => //; rewrite lter_pmul2l //; case: leP.
+by case: (leP (_ * _)); rewrite lter_pmul2l //; case: leP.
 Qed.
 
 Lemma minr_nmulr x y z : x <= 0 -> x * min y z = max (x * y) (x * z).
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index b261072..8f3efaf 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -1216,35 +1216,35 @@ Context {T : latticeType}.
 Definition meet : T -> T -> T := Lattice.meet (Lattice.class T).
 Definition join : T -> T -> T := Lattice.join (Lattice.class T).
 
-Variant lel_xor_gt (x y : T) : bool -> bool -> T -> T -> T -> T -> Set :=
-  | LelNotGt of x <= y : lel_xor_gt x y true false x x y y
-  | GtlNotLe of y < x  : lel_xor_gt x y false true y y x x.
+Variant lel_xor_gt (x y : T) : T -> T -> T -> T -> bool -> bool -> Set :=
+  | LelNotGt of x <= y : lel_xor_gt x y x x y y true false
+  | GtlNotLe of y < x  : lel_xor_gt x y y y x x false true.
 
-Variant ltl_xor_ge (x y : T) : bool -> bool -> T -> T -> T -> T -> Set :=
-  | LtlNotGe of x < y  : ltl_xor_ge x y false true x x y y
-  | GelNotLt of y <= x : ltl_xor_ge x y true false y y x x.
+Variant ltl_xor_ge (x y : T) : T -> T -> T -> T -> bool -> bool -> Set :=
+  | LtlNotGe of x < y  : ltl_xor_ge x y x x y y false true
+  | GelNotLt of y <= x : ltl_xor_ge x y y y x x true false.
 
 Variant comparel (x y : T) :
-  bool -> bool -> bool -> bool -> bool -> bool -> T -> T -> T -> T -> Set :=
+  T -> T -> T -> T -> bool -> bool -> bool -> bool -> bool -> bool -> Set :=
   | ComparelLt of x < y : comparel x y
-    false false false true false true x x y y
+    x x y y false false false true false true
   | ComparelGt of y < x : comparel x y
-    false false true false true false y y x x
+    y y x x false false true false true false
   | ComparelEq of x = y : comparel x y
-    true true true true false false x x x x.
+    x x x x true true true true false false.
 
 Variant incomparel (x y : T) :
-  bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool ->
-  T -> T -> T -> T -> Set :=
+  T -> T -> T -> T ->
+  bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> Set :=
   | InComparelLt of x < y : incomparel x y
-    false false false true false true true true x x y y
+    x x y y false false false true false true true true
   | InComparelGt of y < x : incomparel x y
-    false false true false true false true true y y x x
+    y y x x false false true false true false true true
   | InComparel of x >< y  : incomparel x y
-    false false false false false false false false
     (meet x y) (meet x y) (join x y) (join x y)
+    false false false false false false false false
   | InComparelEq of x = y : incomparel x y
-    true true true true false false true true x x x x.
+    x x x x true true true true false false true true.
 
 End LatticeDef.
 
@@ -3218,8 +3218,8 @@ Lemma leU2 x y z t : x <= z -> y <= t -> x `|` y <= z `|` t.
 Proof. exact: (@leI2 _ [latticeType of L^d]). Qed.
 
 Lemma lcomparableP x y : incomparel x y
-  (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y)
-  (y >=< x) (x >=< y) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+  (y `&` x) (x `&` y) (y `|` x) (x `|` y)
+  (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y) (y >=< x) (x >=< y).
 Proof.
 by case: (comparableP x) => [hxy|hxy|hxy|->]; do 1?have hxy' := ltW hxy;
   rewrite ?(meetxx, joinxx, meetC y, joinC y)
@@ -3228,16 +3228,16 @@ by case: (comparableP x) => [hxy|hxy|hxy|->]; do 1?have hxy' := ltW hxy;
 Qed.
 
 Lemma lcomparable_ltgtP x y : x >=< y ->
-  comparel x y (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y)
-           (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+  comparel x y (y `&` x) (x `&` y) (y `|` x) (x `|` y)
+               (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y).
 Proof. by case: (lcomparableP x) => // *; constructor. Qed.
 
 Lemma lcomparable_leP x y : x >=< y ->
-  lel_xor_gt x y (x <= y) (y < x) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+  lel_xor_gt x y (y `&` x) (x `&` y) (y `|` x) (x `|` y) (x <= y) (y < x).
 Proof. by move/lcomparable_ltgtP => [/ltW xy|xy|->]; constructor. Qed.
 
 Lemma lcomparable_ltP x y : x >=< y ->
-  ltl_xor_ge x y (y <= x) (x < y) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+  ltl_xor_ge x y (y `&` x) (x `&` y) (y `|` x) (x `|` y) (y <= x) (x < y).
 Proof. by move=> /lcomparable_ltgtP [xy|/ltW xy|->]; constructor. Qed.
 
 End LatticeTheoryJoin.
-- 
cgit v1.2.3