case intro.intro
α : Type u
l l' : List α
hd : α
tl : List α
h : hd :: tl ≠ []
⊢ cyclicPermutations (hd :: tl) = dropLast (zipWith (fun x x_1 => x ++ x_1) (tails (hd :: tl)) (inits (hd :: tl)))
α : Type u
l✝ l' l : List α
h : l ≠ []
⊢ cyclicPermutations l = dropLast (zipWith (fun x x_1 => x ++ x_1) (tails l) (inits l))
obtain ⟨hd, tl, rfl⟩ := exists_cons_of_ne_nil h
no goals
case intro.intro
α : Type u
l l' : List α
hd : α
tl : List α
h : hd :: tl ≠ []
⊢ cyclicPermutations (hd :: tl) = dropLast (zipWith (fun x x_1 => x ++ x_1) (tails (hd :: tl)) (inits (hd :: tl)))
exact cyclicPermutations_cons _ _