English
The length of a path p is nonzero if and only if there exist c, e, p' with p = e.toPath.comp p' and p.length = p'.length + 1.
Русский
Длина пути p не равна нулю тогда и только тогда, когда существует вершина c, ребро e: a→c и путь p' such that p = e.toPath.comp p' и p.length = p'.length + 1.
LaTeX
$$$\\forall p:\\; \\mathrm{Path}(a,b):\\; p\\neq \\mathrm{nil} \\iff \\exists c:\\, V,\\; \\exists e:\\, a\\to c,\\; \\exists p': \\mathrm{Path}(c,b),\\; p = e^{\\toPath}.comp p' \\land p.length = p'.length + 1.$$$
Lean4
theorem length_ne_zero_iff_eq_comp (p : Path a b) :
p.length ≠ 0 ↔ ∃ (c : V) (e : a ⟶ c) (p' : Path c b), p = e.toPath.comp p' ∧ p.length = p'.length + 1 :=
by
refine ⟨fun h ↦ ?_, ?_⟩
· have h_len : p.length = (p.length - 1) + 1 := by omega
obtain ⟨c, e, p', hp', rfl⟩ := Path.eq_toPath_comp_of_length_eq_succ p h_len
exact ⟨c, e, p', rfl, by cutsat⟩
· rintro ⟨c, p', e, rfl, h⟩
simp [h]
