feat(Foundations): List.getD_append_cons_length and getD_append_cons_of_ne (supplier for #1037)

Complexity/Foundations/Data/List/Lookup.lean

@@ -23,6 +23,8 @@ import Mathlib.Data.List.OfFn
   and returns a member at its first index.
 * `List.getD_set_self`, `List.getD_set_ne`: reading an updated entry or an unchanged entry.
 * `List.Forall₂.getD`: related lists are related at every in-range defaulted lookup.
+* `List.getD_append_cons_length`, `List.getD_append_cons_of_ne`: reading the entry at index
+  `front.length` of `front ++ x :: back`, and the reads that do not depend on it.
 * `List.forall_mem_set_of_forall_mem`, `List.getD_le_of_forall_le`: preserve invariants under
   updates and bound defaulted reads of numeric register files.
 * `List.getD_map_range`: read a function tabulated over a bounded range.
@@ -51,6 +53,20 @@ theorem List.getD_set_ne {α : Type*} {l : List α} {i j : ℕ} {x d : α} (h :
     (l.set i x).getD j d = l.getD j d := by
   simp only [List.getD_eq_getElem?_getD, List.getElem?_set_ne h]
 
+/-- The entry at index `front.length` of `front ++ x :: back` is `x`. -/
+theorem List.getD_append_cons_length {α : Type*} (front back : List α) (x d : α) :
+    (front ++ x :: back).getD front.length d = x := by
+  simp
+
+/-- Reads of `front ++ x :: back` away from index `front.length` do not depend on `x`. -/
+theorem List.getD_append_cons_of_ne {α : Type*} (front back : List α) (x y d : α) {i : ℕ}
+    (h : i ≠ front.length) : (front ++ x :: back).getD i d = (front ++ y :: back).getD i d := by
+  rcases lt_or_gt_of_ne h with hlt | hgt
+  · rw [List.getD_append _ _ _ _ hlt, List.getD_append _ _ _ _ hlt]
+  · rw [List.getD_append_right _ _ _ _ hgt.le, List.getD_append_right _ _ _ _ hgt.le]
+    obtain ⟨j, hj⟩ : ∃ j, i - front.length = j + 1 := ⟨i - front.length - 1, by omega⟩
+    rw [hj, List.getD_cons_succ, List.getD_cons_succ]
+
 /-- A property of all the entries of a list holds of all the entries of an update by a value
 having it. -/
 theorem List.forall_mem_set_of_forall_mem {α : Type*} {p : α → Prop} {l : List α} {i : ℕ} {x : α}