English
For every i, (scanr f b l)[i]? equals Some (foldr f b (l.drop i)) if i < l.length + 1; otherwise it equals None.
Русский
Для каждого i, если i < l.length + 1, то (scanr f b l)[i]? равно Some (foldr f b (l.drop i)); в противном случае — None.
LaTeX
$$$ \\forall (l : List \\alpha) (f : \\alpha \\rightarrow \\beta \\rightarrow \\beta) (b : \\beta) (i : \\mathbb{N}), (i < l.length + 1) \\Rightarrow (scanr f b l)[i]? = \\mathrm{Some}(foldr f b (l.drop i)).$$$
Lean4
theorem getElem?_scanr {i : ℕ} (h : i < l.length + 1) :
(scanr f b l)[i]? = if i < l.length + 1 then some (foldr f b (l.drop i)) else none := by
split <;> simp_all [getElem_scanr]
