From d60c67b8f33f55e11ca159246d2a447102f10f20 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Fri, 30 Aug 2019 11:30:21 +0200
Subject: 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`.
---
 mathcomp/ssreflect/path.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'mathcomp/ssreflect/path.v')

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.
 
-- 
cgit v1.2.3