English
For a cycle s and a nodup s, the previous element of the reversed cycle at x equals the next element of the original cycle at x, under the appropriate proofs.
Русский
Для цикла s и его аккуратно не повторяющегося обратного цикла, предшествующий элемент обратного цикла равен следующему элементу исходного цикла для данного x, при должных доказательствах.
LaTeX
$$$\forall (hs : Nodup s) (x : \alpha) (hx : x \in s), s.reverse.prev (nodup_reverse_iff.mpr hs) x (mem_reverse_iff.mpr hx) = s.next hs x hx$$$
Lean4
nonrec theorem prev_reverse_eq_next (s : Cycle α) :
∀ (hs : Nodup s) (x : α) (hx : x ∈ s),
s.reverse.prev (nodup_reverse_iff.mpr hs) x (mem_reverse_iff.mpr hx) = s.next hs x hx :=
Quotient.inductionOn' s prev_reverse_eq_next
