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

1 files changed, 4 insertions, 6 deletions

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.