diff options
| author | Kazuhiko Sakaguchi | 2020-11-17 09:29:55 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-11-19 05:24:58 +0900 |
| commit | cdbb52e7c60883b0beee923fdd96baa3e80a1912 (patch) | |
| tree | 8697ff95b789afed939ac3f414539d489d2498e3 /mathcomp/ssreflect/path.v | |
| parent | b3d31c4b66581c78ce23b7fc2e76b41a1a4adf60 (diff) | |
Apply a suggestion from code review
Co-authored-by: Christian Doczkal <christian.doczkal@inria.fr>
Diffstat (limited to 'mathcomp/ssreflect/path.v')
| -rw-r--r-- | mathcomp/ssreflect/path.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |