Lean4
/-- `chain R s` means that `R` holds between adjacent elements of `s`.
`chain R ([a, b, c] : Cycle α) ↔ R a b ∧ R b c ∧ R c a` -/
nonrec def Chain (r : α → α → Prop) (c : Cycle α) : Prop :=
Quotient.liftOn' c
(fun l =>
match l with
| [] => True
| a :: m => IsChain r (a :: m ++ [a]))
fun a b hab =>
propext <| by
rcases a with - | ⟨a, l⟩ <;> rcases b with - | ⟨b, m⟩
· rfl
· have := isRotated_nil_iff'.1 hab
contradiction
· have := isRotated_nil_iff.1 hab
contradiction
· dsimp only
obtain ⟨n, hn⟩ := hab
induction n generalizing a b l m with
| zero =>
simp only [rotate_zero, cons.injEq] at hn
rw [hn.1, hn.2]
| succ d hd =>
rcases l with - | ⟨c, s⟩
· simp only [rotate_cons_succ, nil_append, rotate_singleton, cons.injEq] at hn
rw [hn.1, hn.2]
· rw [Nat.add_comm, ← rotate_rotate, rotate_cons_succ, rotate_zero, cons_append] at hn
rw [← hd c _ _ _ hn]
simp [and_comm]
