English
A nontrivial concatenation p.concat h (with h : G.Adj v w) can be represented as a single cons: there exist x, h' : G.Adj u x and q : G.Walk x w such that p.concat h = cons h' q.
Русский
Непустое конкатенационное выражение p.concat h может быть представлено как один конуст, существует x, h' : G.Adj u x и q : G.Walk x w, такое что p.concat h = cons h' q.
LaTeX
$$$$\forall {u,v,w} (p : G.Walk u v)(h : G.Adj v w),\ ∃ x\, ∃ h' : G.Adj u x\, ∃ q : G.Walk x w,\ p.concat h = cons h' q.$$$$
Lean4
/-- A non-trivial `concat` walk is representable as a `cons` walk. -/
theorem exists_concat_eq_cons {u v w : V} :
∀ (p : G.Walk u v) (h : G.Adj v w), ∃ (x : V) (h' : G.Adj u x) (q : G.Walk x w), p.concat h = cons h' q
| nil, h => ⟨_, h, nil, rfl⟩
| cons h' p, h => ⟨_, h', Walk.concat p h, concat_cons _ _ _⟩
