English
A variant of the prev/next equality specialized to the reversed cycle with explicit conversions.
Русский
Уточнённое равенство prev/next в случае обратного цикла с явными преобразованиями.
LaTeX
$$$\forall {\alpha} (s : Cycle α) (hs : Nodup s.reverse) (x : α) (hx : x ∈ s.reverse), s.reverse.prev hs x hx = s.next (nodup_reverse_iff.mp hs) x (mem_reverse_iff.mp hx)$$$
Lean4
@[simp]
nonrec theorem prev_reverse_eq_next' (s : Cycle α) (hs : Nodup s.reverse) (x : α) (hx : x ∈ s.reverse) :
s.reverse.prev hs x hx = s.next (nodup_reverse_iff.mp hs) x (mem_reverse_iff.mp hx) :=
prev_reverse_eq_next s (nodup_reverse_iff.mp hs) x
(mem_reverse_iff.mp hx)
-- `simp` cannot infer the proofs: see `next_reverse_eq_prev'` for `@[simp]` lemma.
