rdrop_concat_succ — Mathlib

English

Dropping from a concatenation with tail element x shifts the drop by one step: (l ++ [x]).rdrop(n+1) = l.rdrop(n).

Русский

Срез по конкатенации с хвостовым элементом x сдвигает шаг среза на единицу: (l ++ [x]).rdrop(n+1) = l.rdrop(n).

LaTeX

$$$ (l \\,++\\, [x]).rdrop (n+1) = l.rd ro p n $$$

Lean4

@[simp]
theorem rdrop_concat_succ (x : α) : rdrop (l ++ [x]) (n + 1) = rdrop l n := by simp [rdrop_eq_reverse_drop_reverse]

Похожие утверждения