English
The predecessor in the reversed list equals the successor in the original: prev(l.reverse) x = next(l) x.
Русский
Предшественник в перевернутом списке равен последующему в исходном списке: prev(l.reverse) x = next(l) x.
LaTeX
$$$\text{prev}(l.\text{reverse})\ x\ (\text{mem\_reverse.mpr}\ hx) = \text{next}(l)\ x\ hx$$$
Lean4
theorem prev_reverse_eq_next (l : List α) (h : Nodup l) (x : α) (hx : x ∈ l) :
prev l.reverse x (mem_reverse.mpr hx) = next l x hx :=
by
obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
have lpos : 0 < l.length := k.zero_le.trans_lt hk
have key : l.length - 1 - k < l.length := by omega
rw [← getElem_pmap l.next (fun _ h => h) (by simpa using hk)]
simp_rw [getElem_eq_getElem_reverse (l := l), pmap_next_eq_rotate_one _ h]
rw [← getElem_pmap l.reverse.prev fun _ h => h]
· simp_rw [pmap_prev_eq_rotate_length_sub_one _ (nodup_reverse.mpr h), rotate_reverse, length_reverse,
Nat.mod_eq_of_lt (Nat.sub_lt lpos Nat.succ_pos'), Nat.sub_sub_self (Nat.succ_le_of_lt lpos)]
rw [getElem_eq_getElem_reverse]
· simp [Nat.sub_sub_self (Nat.le_sub_one_of_lt hk)]
· simpa
