Commit 2024-10-04 04:46 99b8e711
View on Github →feat(Data/*/Sort): lemmas on sorted lists (#16078)
The main thing we prove is that if l is a list, and a is smaller than all elements on it, then sort r (a :: l) = a :: sort r l.
feat(Data/*/Sort): lemmas on sorted lists (#16078)
The main thing we prove is that if l is a list, and a is smaller than all elements on it, then sort r (a :: l) = a :: sort r l.