rdrop_append_of_le_length — Mathlib

English

If k ≤ length l2, then rdrop (l1 ++ l2) k = l1 ++ rdrop l2 k.

Русский

Если k ≤ длина l2, то rdrop (l1 ++ l2) k = l1 ++ rdrop l2 k.

LaTeX

$$$$ k \le |l_2| \;\Rightarrow\; \mathrm{rdrop}(l_1 ++ l_2)\, k = l_1 ++ \mathrm{rdrop}(l_2)\, k. $$$$

Lean4

theorem rdrop_append_of_le_length {l₁ l₂ : List α} (k : ℕ) :
    k ≤ length l₂ → List.rdrop (l₁ ++ l₂) k = l₁ ++ List.rdrop l₂ k :=
  by
  intro hk
  rw [← length_reverse] at hk
  rw [rdrop_eq_reverse_drop_reverse, reverse_append, drop_append_of_le_length hk, reverse_append, reverse_reverse, ←
    rdrop_eq_reverse_drop_reverse]

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