diff options
| author | Cyril Cohen | 2020-11-19 11:48:46 +0100 |
|---|---|---|
| committer | GitHub | 2020-11-19 11:48:46 +0100 |
| commit | 75da4dbbf2fa6ca6ee150d272d3a793bff63c931 (patch) | |
| tree | 512c6cc466df5609008bb339a1a2a67dd59df44d /mathcomp/ssreflect/fintype.v | |
| parent | 0606b6bf22e258dc3b7cf440f10c108f785904b5 (diff) | |
| parent | 9e6c20b4bd5397539debee9fcb0853b6924ecfb9 (diff) | |
Merge pull request #650 from pi8027/refactor-sorting-lemmas
Refactor, reshuffle, and rename sorting lemmas in `path.v`
Diffstat (limited to 'mathcomp/ssreflect/fintype.v')
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 91d5c80..b125ba5 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -1648,7 +1648,7 @@ pose t0 := nth (F i0) s 0; have: t0 \in s by rewrite mem_nth. rewrite mem_sort => /mapP/sig2_eqW[it0]; rewrite mem_enum => it0P def_t0. have /negP[/=] := no_i it0; rewrite [P _]it0P/=; apply/'forall_implyP=> j Pj. have /(nthP (F i0))[k g_lt <-] : F j \in s by rewrite mem_sort map_f ?mem_enum. -by rewrite -def_t0 sorted_le_nth. +by rewrite -def_t0 sorted_leq_nth. Qed. End Extremum. |