feat(Combinatorics/SimpleGraph/Walk): a vertex of a walk is in its tail starting from the second vertex onwards (#31119)

Add helper theorems for #29309

Author: LLaurance

Mathlib/Combinatorics/SimpleGraph/Walk.lean

@@ -948,6 +948,9 @@ abbrev snd (p : G.Walk u v) : V := p.getVert 1
 lemma snd_cons {u v w} (q : G.Walk v w) (hadj : G.Adj u v) :
     (q.cons hadj).snd = v := by simp
 
+lemma snd_mem_tail_support {u v : V} {p : G.Walk u v} (h : ¬p.Nil) : p.snd ∈ p.support.tail :=
+  p.notNilRec (by simp) h
+
 /-- The walk obtained by taking the first `n` darts of a walk. -/
 def take {u v : V} (p : G.Walk u v) (n : ℕ) : G.Walk u (p.getVert n) :=
   match p, n with
@@ -1141,6 +1144,12 @@ theorem exists_boundary_dart {u v : V} (p : G.Walk u v) (S : Set V) (uS : u ∈
     p.tail.getVert n = p.getVert (n + 1) := by
   cases p <;> simp
 
+lemma getVert_mem_tail_support {u v : V} {p : G.Walk u v} (hp : ¬p.Nil) :
+    ∀ {i : ℕ}, i ≠ 0 → p.getVert i ∈ p.support.tail
+  | i + 1, _ => by
+    rw [← getVert_tail, ← p.support_tail_of_not_nil hp]
+    exact getVert_mem_support ..
+
 lemma ext_support {u v} {p q : G.Walk u v} (h : p.support = q.support) :
     p = q := by
   induction q with