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

4 files changed, 31 insertions, 19 deletions

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.