English
IsChain R on the reverse of a list is equivalent to IsChain on the original list with the relation flipped.
Русский
Цепь по R на обратном списке эквивалентна цепи по перевернутому отношению на исходном списке.
LaTeX
$$$IsChain\\, R\\, (\\text{reverse } l) \\iff IsChain\\, (\\text{flip } R)\\, l$$$
Lean4
theorem isChain_reverse {l : List α} : IsChain R (reverse l) ↔ IsChain (flip R) l := by
induction l using twoStepInduction with
| nil => grind
| singleton a => grind
| cons_cons a b l IH IH2 =>
rw [isChain_cons_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append, isChain_split, ←
reverse_cons, IH2, and_comm, isChain_pair, flip]
