English
In a Nodup list, applying next after prev recovers the original element: prev(l.next x hx) = x.
Русский
В списке без повторов применение next после prev возвращает исходный элемент: prev(l.next x hx) = x.
LaTeX
$$$prev\ l\ (next\ l\ x\ hx)\ (next\_mem\ _\ _ ) = x$$$
Lean4
theorem prev_next (l : List α) (h : Nodup l) (x : α) (hx : x ∈ l) : prev l (next l x hx) (next_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 + 1 + length tl) % (length tl + 1) = n :=
by
rw [length_cons] at hn
rw [add_assoc, add_comm 1, Nat.add_mod_right, Nat.mod_eq_of_lt hn]
simp only [length_cons, Nat.succ_sub_succ_eq_sub, Nat.sub_zero, this]
