English
For a nonempty list l, the chain on the cycle built from l is equivalent to a chain on the list obtained by placing the last element in front.
Русский
Для непустого списка l цепь на цикле, построенном из l, эквивалентна цепи на списке, где последний элемент помещён вперед.
LaTeX
$$$$ \\forall l\\neq\\emptyset,\\; Cycle.Chain\\ r\\ (Cycle.ofList\\ l) \\iff List.IsChain\\ r\\ (getLast\\ l\\ hl :: l). $$$$
Lean4
theorem chain_ne_nil (r : α → α → Prop) {l : List α} : ∀ hl : l ≠ [], Chain r l ↔ List.IsChain r (getLast l hl :: l) :=
l.reverseRecOn (fun hm => hm.irrefl.elim)
(by
intro m a _H _
rw [← coe_cons_eq_coe_append, chain_coe_cons, getLast_append_singleton])
