Commit 2024-07-20 10:12 8ddfa156

feat(Order/Interval/Finset/Nat): Icc_insert_succ_left, Icc_insert_succ_right (#14838) Add two more lemmas about inserting an element just before or after an interal in ℕ:

lemma Icc_insert_succ_left (h : a ≤ b) : insert a (Icc (a + 1) b) = Icc a b := by
lemma Icc_insert_succ_right (h : a ≤ b + 1) : insert (b + 1) (Icc a b) = Icc a (b + 1) := by