English
If p.length ≤ p.bypass.length, then p.bypass = p.
Русский
Если длина обхода не больше длины обхода, то обход равен своему обходу.
LaTeX
$$$ \forall {V} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} (p : G.Walk u v), p.length \le p.bypass.length \to p.bypass = p$$$
Lean4
theorem bypass_eq_self_of_length_le {u v : V} (p : G.Walk u v) (h : p.length ≤ p.bypass.length) : p.bypass = p := by
induction p with
| nil => rfl
| cons h p ih =>
simp only [Walk.bypass]
split_ifs with hb
· exfalso
simp only [hb, Walk.bypass, Walk.length_cons, dif_pos] at h
apply Nat.not_succ_le_self p.length
calc
p.length + 1
_ ≤ (p.bypass.dropUntil _ _).length := h
_ ≤ p.bypass.length := (Walk.length_dropUntil_le p.bypass hb)
_ ≤ p.length := Walk.length_bypass_le _
· simp only [hb, Walk.bypass, Walk.length_cons, not_false_iff, dif_neg, Nat.add_le_add_iff_right] at h
rw [ih h]
