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

State before:
α : Type u_1
xs ys : List α
⊢ drop (length xs) (xs ++ ys) = ys
Tactic:
apply list_drop_length_prefix_is_suffix
State after:
no goals