From cdbb52e7c60883b0beee923fdd96baa3e80a1912 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 17 Nov 2020 09:29:55 +0900 Subject: Apply a suggestion from code review Co-authored-by: Christian Doczkal --- mathcomp/ssreflect/path.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 1bec943..42d93f0 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -1044,7 +1044,7 @@ Lemma sort_stable T (leT leT' : rel T) : Proof. move=> leT_total leT'_tr s sorted_s; case Ds: s => // [x s1]. rewrite -{s1}Ds -(mkseq_nth x s) sort_map. -have leN_total: total (xrelpre (nth x s) leT) by move=> n m; apply: leT_total. +have leN_total: total (relpre (nth x s) leT) by move=> n m; apply: leT_total. apply: (homo_sorted_in _ (allss _)) (sort_iota_stable leN_total _) => /= y z. rewrite !mem_sort !mem_iota !leq0n add0n /= => ys zs /andP [->] /=. by case: (leT _ _); first apply: sorted_ltn_nth. -- cgit v1.2.3