case h
α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
hs : Nodup (Quot.mk Setoid.r a✝)
hx : x ∈ Quot.mk Setoid.r a✝
⊢ next (Quot.mk Setoid.r a✝) hs x hx ∈ Quot.mk Setoid.r a✝
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : Nodup s
x : α
hx : x ∈ s
⊢ next s hs x hx ∈ s
induction s using Quot.inductionOn
case h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
hs : Nodup (Quot.mk Setoid.r a✝)
hx : x ∈ Quot.mk Setoid.r a✝
⊢ x ∈ a✝
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
hs : Nodup (Quot.mk Setoid.r a✝)
hx : x ∈ Quot.mk Setoid.r a✝
⊢ next (Quot.mk Setoid.r a✝) hs x hx ∈ Quot.mk Setoid.r a✝
apply next_mem
no goals
case h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
hs : Nodup (Quot.mk Setoid.r a✝)
hx : x ∈ Quot.mk Setoid.r a✝
⊢ x ∈ a✝
assumption