feat: add lemmas about lists

I need these lemmas to prove `String.splitOn_of_valid`.

Batteries/Data/List/Lemmas.lean

@@ -19,6 +19,11 @@ namespace List
 
 @[deprecated (since := "2024-08-15")] alias isEmpty_iff_eq_nil := isEmpty_iff
 
+/-! ### head and tail -/
+
+theorem head_cons_tail : ∀ l h, @head α l h :: l.tail = l
+  | _::_, _ => rfl
+
 /-! ### next? -/
 
 @[simp] theorem next?_nil : @next? α [] = none := rfl
@@ -482,6 +487,12 @@ theorem Sublist.erase_diff_erase_sublist {a : α} :
 
 end Diff
 
+/-! ### prefix, suffix, infix -/
+
+theorem ne_nil_of_not_prefix (h : ¬l₁ <+: l₂) : l₁ ≠ [] := by
+  intro heq
+  simp [heq, nil_prefix] at h
+
 /-! ### drop -/
 
 theorem disjoint_take_drop : ∀ {l : List α}, l.Nodup → m ≤ n → Disjoint (l.take m) (l.drop n)