Theorem: List.lastN_zero (One.lean)

State before:
α : Type u_1
l : List α
⊢ lastN 0 l = []
Tactic:
unfold List.lastN
State after:
α : Type u_1
l : List α
⊢ drop (length l - 0) l = []

State before:
α : Type u_1
l : List α
⊢ drop (length l - 0) l = []
Tactic:
simp
State after:
no goals