English
Let p be a walk from v to u and h an edge from u to v. Then the walk formed by prepending h to p is a cycle if and only if p is a path and the edge {u,v} does not already appear in p.
Русский
Пусть p — ход от v к u, а h — ребро u~v. Нужно, чтобы Walk.cons h p образовала цикл тогда и только тогда, когда p является путём и ребро {u,v} не встречается в p.
LaTeX
$$$(Walk.cons h p).IsCycle \iff p.IsPath \land s(u,v) \notin p.edges$$$
Lean4
theorem cons_isCycle_iff {u v : V} (p : G.Walk v u) (h : G.Adj u v) :
(Walk.cons h p).IsCycle ↔ p.IsPath ∧ s(u, v) ∉ p.edges :=
by
simp only [Walk.isCycle_def, Walk.isPath_def, Walk.isTrail_def, edges_cons, List.nodup_cons, support_cons,
List.tail_cons]
have : p.support.Nodup → p.edges.Nodup := edges_nodup_of_support_nodup
tauto
