English
For a cycle p, the vertices of getVert are pairwise distinct on the interior indices 1 ≤ i ≤ length(p) − 1.
Русский
Для цикла p вершины на внутренних индексах 1 ≤ i ≤ length(p) − 1 попарно различны.
LaTeX
$$p.IsCycle \Rightarrow Set.InjOn p.getVert {i | 1 \le i \le p.length - 1}$$
Lean4
theorem getVert_injOn {p : G.Walk u u} (hpc : p.IsCycle) : Set.InjOn p.getVert {i | 1 ≤ i ∧ i ≤ p.length} :=
by
rw [← p.cons_tail_eq hpc.not_nil] at hpc
intro n hn m hm hnm
rw [← SimpleGraph.Walk.length_tail_add_one (p.not_nil_of_tail_not_nil (not_nil_of_isCycle_cons hpc)),
Set.mem_setOf] at hn hm
have :=
((Walk.cons_isCycle_iff _ _).mp hpc).1.getVert_injOn (by cutsat : n - 1 ≤ p.tail.length)
(by cutsat : m - 1 ≤ p.tail.length)
(by simp_all [SimpleGraph.Walk.getVert_tail, Nat.sub_add_cancel hn.1, Nat.sub_add_cancel hm.1])
omega
