α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : Nodup s
x : α
hx : x ∈ s
⊢ next (reverse s) (_ : Nodup (reverse s)) x (_ : x ∈ reverse s) ∈ reverse s
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : Nodup s
x : α
hx : x ∈ s
⊢ prev s hs x hx ∈ s
rw [← next_reverse_eq_prev, ← mem_reverse_iff]
no goals
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : Nodup s
x : α
hx : x ∈ s
⊢ next (reverse s) (_ : Nodup (reverse s)) x (_ : x ∈ reverse s) ∈ reverse s
apply next_mem