English
If l is rotated to l' (l ~r l'), then for any x ∈ l, the next element after x in l equals the next element after x in l' (with the corresponding membership transfer).
Русский
Если список l получен поворотом в l' (l ~r l'), то для любого x ∈ l следующий за x в l равен следующему за x в l' (с соответствующим переносом принадлежности).
LaTeX
$$$\forall x\ hvhx:\ x\in l,\ next\ l\ x\ hx = next\ l'\ x\ (h.mem\_iff.mp hx)$$$
Lean4
theorem isRotated_next_eq {l l' : List α} (h : l ~r l') (hn : Nodup l) {x : α} (hx : x ∈ l) :
l.next x hx = l'.next x (h.mem_iff.mp hx) :=
by
obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
obtain ⟨n, rfl⟩ := id h
rw [next_getElem _ hn]
simp_rw [getElem_eq_getElem_rotate _ n k]
rw [next_getElem _ (h.nodup_iff.mp hn), getElem_eq_getElem_rotate _ n]
simp [add_assoc]
