feat: Add getVert_append and getVert_reverse (#11787)

Author: IvanRenison

Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

@@ -430,6 +430,28 @@ theorem exists_length_eq_zero_iff {u v : V} : (∃ p : G.Walk u v, p.length = 0)
 theorem length_eq_zero_iff {u : V} {p : G.Walk u u} : p.length = 0 ↔ p = nil := by cases p <;> simp
 #align simple_graph.walk.length_eq_zero_iff SimpleGraph.Walk.length_eq_zero_iff
 
+theorem getVert_append {u v w : V} (p : G.Walk u v) (q : G.Walk v w) (i : ℕ) :
+    (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length) := by
+  induction p generalizing i with
+  | nil => simp
+  | cons h p ih => cases i <;> simp [getVert, ih, Nat.succ_lt_succ_iff]
+
+theorem getVert_reverse {u v : V} (p : G.Walk u v) (i : ℕ) :
+    p.reverse.getVert i = p.getVert (p.length - i) := by
+  induction p with
+  | nil => rfl
+  | cons h p ih =>
+    simp only [reverse_cons, getVert_append, length_reverse, ih, length_cons]
+    split_ifs
+    next hi =>
+      rw [Nat.succ_sub hi.le]
+      simp [getVert]
+    next hi =>
+      obtain rfl | hi' := Nat.eq_or_lt_of_not_lt hi
+      · simp [getVert]
+      · rw [Nat.eq_add_of_sub_eq (Nat.sub_pos_of_lt hi') rfl, Nat.sub_eq_zero_of_le hi']
+        simp [getVert]
+
 section ConcatRec
 
 variable {motive : ∀ u v : V, G.Walk u v → Sort*} (Hnil : ∀ {u : V}, motive u u nil)