Theorem: list_drop_app (Katydid/Std/Lists.lean)

State before:
α : Type u_1
n : ℕ
xs ys : List α
⊢ drop n (xs ++ ys) = drop n xs ++ drop (n - length xs) ys
Tactic:
sorry
State after:
no goals