Change the order of arguments in `ltngtP`

from
`ltngtP m n : compare_nat m n (m <= n) (n <= m) (m < n) (n < m) (n == m) (m == n)`
to
`ltngtP m n : compare_nat m n (n == m) (m == n) (n <= m) (m <= n) (n < m) (m < n)`,
to make it tries to match subterms with `m < n` first, `m <= n`, then `m == n`.

10 files changed, 42 insertions, 30 deletions

diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v
index b65742d..aa076a2 100644
--- a/mathcomp/algebra/polydiv.v
+++ b/mathcomp/algebra/polydiv.v
@@ -3243,7 +3243,7 @@ move=> hsp /=; have [->|p_neq0] := altP (p =P 0).
   by rewrite size_poly0 expr0 mulr1 dvd0p=> /(_ isT).
 have [|ncop_pq] := boolP (coprimep _ _); first by rewrite dvdp_mulr ?dvdpp.
 have g_gt1: (1 < size (gcdp p q))%N.
-  have [|//|/eqP] := ltngtP; last by rewrite -coprimep_def (negPf ncop_pq).
+  have [//||/esym/eqP] := ltngtP; last by rewrite -coprimep_def (negPf ncop_pq).
   by rewrite ltnS leqn0 size_poly_eq0 gcdp_eq0 (negPf p_neq0).
 have sd : (size (p %/ gcdp p q) < size p)%N.
   rewrite size_divp -?size_poly_eq0 -(subnKC g_gt1) // add2n /=.
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index 3c4c002..2a17a4a 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -138,9 +138,9 @@ Lemma oppzK : involutive oppz. Proof. by do 2?case. Qed.
 
 Lemma oppz_add : {morph oppz : m n / m + n}.
 Proof.
-move=> [[|n]|n] [[|m]|m] /=; rewrite ?NegzE ?oppzK ?addnS ?addn0 ?subn0 //;
-  rewrite ?ltnS[m <= n]leqNgt [n <= m]leqNgt; case: ltngtP=> hmn /=;
-    by rewrite ?hmn ?subnn // ?oppzK ?subSS ?subnS ?prednK // ?subn_gt0.
+by move=> [[|n]|n] [[|m]|m] /=; rewrite ?addn0 ?subn0 ?addnS //;
+  rewrite !NegzE !ltnS !subSS; case: ltngtP => [?|?|->];
+  rewrite ?subnn // ?oppzK ?subnS ?prednK // subn_gt0.
 Qed.
 
 Lemma add1Pz (n : int) : 1 + (n - 1) = n.
@@ -154,9 +154,9 @@ Qed.
 Lemma addSnz (m : nat) (n : int) : (m.+1%N) + n = 1 + (m + n).
 Proof.
 move: m n=> [|m] [] [|n] //=; rewrite ?add1n ?subn1 // !(ltnS, subSS).
-rewrite [n <= m]leqNgt; case: ltngtP=> hmn /=; rewrite ?hmn ?subnn //.
+case: ltngtP=> hnm /=; rewrite ?hnm ?subnn //.
   by rewrite subnS add1n prednK ?subn_gt0.
-by rewrite ltnS leqn0 subn_eq0 leqNgt hmn /= subnS subn1.
+by rewrite ltnS leqn0 subn_eq0 leqNgt hnm /= subnS subn1.
 Qed.
 
 Lemma addSz (m n : int) : (1 + m) + n = 1 + (m + n).
diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v
index 3f25ae6..f494a09 100644
--- a/mathcomp/field/algnum.v
+++ b/mathcomp/field/algnum.v
@@ -823,7 +823,7 @@ rewrite /orderC; case: pickP => /= [k /eqP Dp_k | no_k]; last first.
   rewrite mem_primes => /and3P[q_pr _ q_dv_m].
   rewrite lognE q_pr m_gt0 q_dv_m /=; move: (logn q _) => k.
   rewrite !mulnA expnS leq_mul //.
-  case: (ltngtP q) => // [|q_gt2 | ->]; first by rewrite ltnNge prime_gt1.
+  case: (ltngtP q 2) (prime_gt1 q_pr) => // [q_gt2|->] _.
     rewrite mul1n mulnAC mulnn -{1}[q]muln1 leq_mul ?expn_gt0 ?prime_gt0 //.
     by rewrite -(subnKC q_gt2) (ltn_exp2l 1).
   by rewrite !muln1 -expnS (ltn_exp2l 0).
diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v
index 2e025a2..8c2badb 100644
--- a/mathcomp/solvable/abelian.v
+++ b/mathcomp/solvable/abelian.v
@@ -1742,8 +1742,8 @@ have cnt_b b: \big[dprod/1]_(x <- b) <[x]> = G ->
   count [pred x | #[x] == p ^ k.+1]%N b = cnt_p k b - cnt_p k.+1 b.
 - move/p_bG; elim: b => //= _ b IHb /andP[/p_natP[j ->] /IHb-> {IHb}].
   rewrite eqn_leq !leq_exp2l ?prime_gt1 // -eqn_leq pfactorK //.
-  case: ltngtP => // _ {j}; rewrite subSn // add0n; elim: b => //= y b IHb.
-  by rewrite leq_add // ltn_neqAle; case: (~~ _).
+  case: (ltngtP k.+1) => // _ {j}; rewrite subSn // add0n.
+  by elim: b => //= y b IHb; rewrite leq_add // ltn_neqAle; case: (~~ _).
 by rewrite !cnt_b // /cnt_p !(@count_logn_dprod_cycle _ _ _ G).
 Qed.
 
diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v
index 18c6509..efbe824 100644
--- a/mathcomp/solvable/burnside_app.v
+++ b/mathcomp/solvable/burnside_app.v
@@ -436,7 +436,7 @@ Qed.
 Lemma card_n3 : forall x y : square, x != y ->
   #|[set k : col_squares | k x == k y]| = (n ^ 3)%N.
 Proof.
-move=> x y nxy; apply/eqP; case: (ltngtP n 0) => // [|n0]; last first.
+move=> x y nxy; apply/eqP; case: (posnP n) => [n0|].
   by rewrite n0; apply/existsP=> [] [p _]; case: (p c0) => i; rewrite n0.
 move/eqn_pmul2l <-; rewrite -expnS -card_Fid Fid cardsT.
 rewrite -{1}[n]card_ord -cardX.
diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v
index d236575..be885b1 100644
--- a/mathcomp/solvable/extremal.v
+++ b/mathcomp/solvable/extremal.v
@@ -1831,7 +1831,7 @@ case/pred2P: Z_xxy => xy; last first.
   have n_gt3: n > 3.
     case: ltngtP notXy => // [|n3]; first by rewrite ltnNge n_gt2.
     rewrite -scXG inE Gy defX cent_cycle; case/cent1P; red.
-    by rewrite (conjgC x) xy /r p2 n3.
+    by rewrite (conjgC x) xy /r p2 -n3.
   exists n => //; rewrite isogEcard card_semidihedral // oG p2 leqnn andbT.
   rewrite Grp_semidihedral //; apply/existsP=> /=.
   case/pred2P: Zy2 => y2; [exists (x, y) | exists (x, x * y)].
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index f757e94..0da7a16 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -1004,7 +1004,7 @@ Proof. by elim: n x => //= n IHn x //=; rewrite IHn. Qed.
 
 Lemma nth_traject i n : i < n -> forall x, nth x (traject x n) i = iter i f x.
 Proof.
-elim: n => // n IHn; rewrite ltnS leq_eqVlt => le_i_n x.
+elim: n => // n IHn; rewrite ltnS => le_i_n x.
 rewrite trajectSr nth_rcons size_traject.
 by case: ltngtP le_i_n => [? _||->] //; apply: IHn.
 Qed.
@@ -1086,8 +1086,8 @@ Proof.
 move=> x; rewrite prev_nth mem_next next_nth; case p_x: (x \in p) => //.
 case def_p: p Up p_x => // [y q]; rewrite -{-1}def_p => /= /andP[not_qy Uq] p_x.
 rewrite -{2}(nth_index y p_x); congr (nth y _ _); set i := index x p.
-have: ~~ (size q < i) by rewrite -index_mem -/i def_p leqNgt in p_x.
-case: ltngtP => // [lt_i_q | ->] _; first by rewrite index_uniq.
+have: i <= size q by rewrite -index_mem -/i def_p in p_x.
+case: ltngtP => // [lt_i_q|->] _; first by rewrite index_uniq.
 by apply/eqP; rewrite nth_default // eqn_leq index_size leqNgt index_mem.
 Qed.
 
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 9eafea9..1185e67 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -579,7 +579,7 @@ Qed.
 Lemma coprime_has_primes m n :
   0 < m -> 0 < n -> coprime m n = ~~ has (mem (primes m)) (primes n).
 Proof.
-move=> m_gt0 n_gt0; apply/eqnP/hasPn=> [mn1 p | no_p_mn].
+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.
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index c45f7fc..35d9a69 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -725,16 +725,14 @@ Proof. by move <-; elim: s1 => [|x s1 IHs]; rewrite ?take0 //= IHs. Qed.
 
 Lemma takel_cat s1 s2 : n0 <= size s1 -> take n0 (s1 ++ s2) = take n0 s1.
 Proof.
-by rewrite take_cat; case: ltngtP => // <-; rewrite subnn take0 take_size cats0.
+by rewrite take_cat; case: ltngtP => // ->; rewrite subnn take0 take_size cats0.
 Qed.
 
 Lemma nth_drop s i : nth (drop n0 s) i = nth s (n0 + i).
 Proof.
-have [lt_n0_s | le_s_n0] := ltnP n0 (size s).
-  rewrite -{2}[s]cat_take_drop nth_cat size_take lt_n0_s /= addKn.
-  by rewrite ltnNge leq_addr.
-rewrite !nth_default //; first exact: leq_trans (leq_addr _ _).
-by rewrite size_drop (eqnP le_s_n0).
+rewrite -{2}[s]cat_take_drop nth_cat size_take ltnNge.
+case: ltnP => [?|le_s_n0]; rewrite ?(leq_trans le_s_n0) ?leq_addr ?addKn //=.
+by rewrite drop_oversize // !nth_default.
 Qed.
 
 Lemma nth_take i : i < n0 -> forall s, nth (take n0 s) i = nth s i.
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 39131f0..f358f7b 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -446,7 +446,7 @@ Variant ltn_xor_geq m n : bool -> bool -> Set :=
   | 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 rewrite -(ltnS n); case: leqP; constructor. Qed.
+Proof. by case: leqP; constructor. Qed.
 
 Variant eqn0_xor_gt0 n : bool -> bool -> Set :=
   | Eq0NotPos of n = 0 : eqn0_xor_gt0 n true false
@@ -457,18 +457,18 @@ 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 true false true false false false
-  | CompareNatGt of m > n : compare_nat m n false true false true false false
-  | CompareNatEq of m = n : compare_nat m n true true false false true true.
+  | 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 (m <= n) (n <= m) (m < n)
-                                   (n < m) (n == m) (m == n).
+Lemma ltngtP m n : compare_nat m n (n == m) (m == n) (n <= m)
+                                   (m <= n) (n < m) (m < n).
 Proof.
-rewrite !ltn_neqAle [_ == m]eq_sym; case: ltnP => [mn|].
+rewrite !ltn_neqAle [_ == n]eq_sym; case: ltnP => [nm|].
   by rewrite ltnW // gtn_eqF //; constructor.
-rewrite leq_eqVlt; case: ltnP; rewrite ?(orbT, orbF) => //= lt_nm eq_mn.
+rewrite leq_eqVlt; case: ltnP; rewrite ?(orbT, orbF) => //= lt_mn eq_nm.
   by rewrite ltn_eqF //; constructor.
-by rewrite eq_mn; constructor; apply/eqP.
+by rewrite eq_nm; constructor; apply/esym/eqP.
 Qed.
 
 (* Monotonicity lemmas *)
@@ -1795,3 +1795,17 @@ Ltac nat_congr := first
      apply: (congr1 (addn X1) _);
      symmetry
    end ].
+
+Module mc_1_9.
+
+Variant compare_nat m n :
+   bool -> bool -> bool -> bool -> bool -> bool -> Set :=
+  | CompareNatLt of m < n : compare_nat m n true false true false false false
+  | CompareNatGt of m > n : compare_nat m n false true false true false false
+  | CompareNatEq of m = n : compare_nat m n true true false false true true.
+
+Lemma ltngtP m n : compare_nat m n (m <= n) (n <= m) (m < n)
+                                   (n < m) (n == m) (m == n).
+Proof. by case: ltngtP; constructor. Qed.
+
+End mc_1_9.