Theorem: List.drop_cons (One.lean)

State before:
α : Type u_1
n : ℕ
head : α
tail : List α
⊢ drop (n + 1) (head :: tail) = drop n tail
Tactic:
simp only [drop, zero_le, ge_iff_le, nonpos_iff_eq_zero, Nat.add_eq, add_zero]
State after:
no goals