case h
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
a✝ : List α
h : Nodup (Quot.mk Setoid.r a✝)
hn : Nontrivial (Quot.mk Setoid.r a✝)
⊢ IsCycle (formPerm (Quot.mk Setoid.r a✝) h)
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
h : Nodup s
hn : Nontrivial s
⊢ IsCycle (formPerm s h)
induction s using Quot.inductionOn
no goals
case h
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
a✝ : List α
h : Nodup (Quot.mk Setoid.r a✝)
hn : Nontrivial (Quot.mk Setoid.r a✝)
⊢ IsCycle (formPerm (Quot.mk Setoid.r a✝) h)
exact List.isCycle_formPerm h (length_nontrivial hn)