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

State before:
α : Type u
n : ℕ
⊢ drop n [] = []
Tactic:
cases n with
| zero => rw [drop]
| succ n' => rw [drop]
State after:
no goals

State before:
case zero
α : Type u
⊢ drop zero [] = []
Tactic:
rw [drop]
State after:
no goals

State before:
case succ
α : Type u
n' : ℕ
⊢ drop (succ n') [] = []
Tactic:
rw [drop]
State after:
no goals