Commit 2023-02-18 18:11 4557f2c4

feat: add lemmas about List.Sorted (#2311)

• Add List.Sorted.le_of_lt and List.Sorted.lt_of_le (new).
• Add List.Sorted.rel_get_of_lt and List.Sorted.rel_get_of_le (get versions of nthLe lemmas).
• Add List.sorted_ofFn_iff, List.sorted_lt_ofFn_iff, and List.sorted_le_ofFn_iff (new).
• Deprecate List.monotone_iff_ofFn_sorted in favor of List.sorted_le_ofFn_iff.
• Rename List.Monotone.ofFn_sorted to Monotone.ofFn_sorted. In Lean 3, dot notation hf.of_fn_sorted used lift.monotone.of_fn_sorted if the list namespace is open. This is no longer the case in Lean 4.