diff options
| author | Kazuhiko Sakaguchi | 2019-08-30 11:30:21 +0200 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2019-10-30 23:19:33 +0100 |
| commit | d60c67b8f33f55e11ca159246d2a447102f10f20 (patch) | |
| tree | 74fecfdcc5b2429e5cf199f9daa48a56540e2359 /mathcomp/ssreflect/path.v | |
| parent | c5bd1d4d29021688db59495a8b60c84f5dea6b77 (diff) | |
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`.
Diffstat (limited to 'mathcomp/ssreflect/path.v')
| -rw-r--r-- | mathcomp/ssreflect/path.v | 6 |
1 files changed, 3 insertions, 3 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. |