English
Given a path p from a to b and any integer n with n ≤ length(p), there exist a vertex v and subpaths p1: a→v, p2: v→b such that p = p1 ∘ p2 and p1 has length n.
Русский
Для пути p от a к b и любого n ≤ length(p) существует вершина v и подпути p1: a→v, p2: v→b такие, что p = p1 ∘ p2 и length(p1) = n.
LaTeX
$$$\exists v\, \exists p_1 : Path\ a\ v\, \exists p_2 : Path\ v\ b,\; p = p_1.comp p_2 \land p_1.length = n$$$
Lean4
/-- Given a path `p : Path a b` and an index `n ≤ p.length`,
we can split `p = p₁.comp p₂` with `p₁.length = n`. -/
theorem exists_eq_comp_of_le_length {n : ℕ} (hn : n ≤ p.length) :
∃ (v : V) (p₁ : Path a v) (p₂ : Path v b), p = p₁.comp p₂ ∧ p₁.length = n := by
induction p generalizing n with
| nil =>
obtain ⟨rfl⟩ : n = 0 := by simpa using hn
exact ⟨a, Path.nil, Path.nil, by simp, rfl⟩
| @cons _ c p' e ih =>
rw [length_cons] at hn
rcases (Nat.le_succ_iff).1 hn with h | rfl
· obtain ⟨d, p₁, p₂, hp, hl⟩ := ih h
exact ⟨d, p₁, p₂.cons e, by simp [hp], hl⟩
· exact ⟨c, p'.cons e, Path.nil, by simp, by simp⟩
