Commit 2023-10-23 16:32 7db2b0a8

feat: two small lemmas about ordered lists (#7829) We prove that in a sorted list, the head! is the smallest element, and that if a list is lexicographically smaller than another list, then its head! is smaller than or equal to that of the other.