Lean4
/-- Given a `s : Cycle α` such that `Nodup s`, retrieve the next element after `x ∈ s`. -/
nonrec def next : ∀ (s : Cycle α) (_hs : Nodup s) (x : α) (_hx : x ∈ s), α := fun s =>
Quot.hrecOn (motive := fun (s : Cycle α) => ∀ (_hs : Cycle.Nodup s) (x : α) (_hx : x ∈ s), α) s
(fun l _hn x hx => next l x hx) fun l₁ l₂ h =>
Function.hfunext (propext h.nodup_iff) fun h₁ h₂ _he =>
Function.hfunext rfl fun x y hxy =>
Function.hfunext (propext (by rw [eq_of_heq hxy]; simpa [eq_of_heq hxy] using h.mem_iff)) fun hm hm' he' =>
heq_of_eq (by rw [heq_iff_eq] at hxy; subst x; simpa using isRotated_next_eq h h₁ _)
