English
In a Nodup list, applying prev after next also recovers the original element: next l (prev l x hx) = x.
Русский
В списке без повторов применение prev после next также возвращает исходный элемент: next(l, prev(l, x hx)) = x.
LaTeX
$$$next\ l\ (prev\ l\ x\ hx)\ (prev\_mem\ _\ _ ) = x$$$
Lean4
theorem next_prev (l : List α) (h : Nodup l) (x : α) (hx : x ∈ l) : next l (prev l x hx) (prev_mem _ _ _) = x :=
by
obtain ⟨n, hn, rfl⟩ := getElem_of_mem hx
simp only [next_getElem, prev_getElem, h, Nat.mod_add_mod]
rcases l with - | ⟨hd, tl⟩
· simp at hn
· have : (n + length tl + 1) % (length tl + 1) = n :=
by
rw [length_cons] at hn
rw [add_assoc, Nat.add_mod_right, Nat.mod_eq_of_lt hn]
simp [this]
