α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l l' : List α
h : l ~r l'
hn : Nodup l
x : α
hx : x ∈ l
⊢ next (reverse l) x (_ : x ∈ reverse l) = next (reverse l') x (_ : x ∈ reverse l')
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l l' : List α
h : l ~r l'
hn : Nodup l
x : α
hx : x ∈ l
⊢ prev l x hx = prev l' x (_ : x ∈ l')
rw [← next_reverse_eq_prev _ hn, ← next_reverse_eq_prev _ (h.nodup_iff.mp hn)]
no goals
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l l' : List α
h : l ~r l'
hn : Nodup l
x : α
hx : x ∈ l
⊢ next (reverse l) x (_ : x ∈ reverse l) = next (reverse l') x (_ : x ∈ reverse l')
exact isRotated_next_eq h.reverse (nodup_reverse.mpr hn) _