feat(Data/List): add theorem length_eq_two' (leanprover-community#35775)

Author: IvanRenison

Mathlib/Data/List/Basic.lean

@@ -120,6 +120,9 @@ lemma length_injective [Subsingleton α] : Injective (length : List α → ℕ)
 theorem length_eq_two {l : List α} : l.length = 2 ↔ ∃ a b, l = [a, b] :=
   ⟨fun _ => let [a, b] := l; ⟨a, b, rfl⟩, fun ⟨_, _, e⟩ => e ▸ rfl⟩
 
+theorem length_eq_two' {l : List α} (h : l ≠ []) : l.length = 2 ↔ l = [l.head h, l.getLast h] := by
+  rw [length_eq_two]; grind
+
 theorem length_eq_three {l : List α} : l.length = 3 ↔ ∃ a b c, l = [a, b, c] :=
   ⟨fun _ => let [a, b, c] := l; ⟨a, b, c, rfl⟩, fun ⟨_, _, _, e⟩ => e ▸ rfl⟩