Theorem: LoVe.drop_drop (LoVe/Labs/Lab4Solution.lean)

State before:
α : Type
n : ℕ
xs : List α
⊢ drop n (drop 0 xs) = drop (n + 0) xs
Tactic:
rfl
State after:
no goals

State before:
α : Type
n✝ x✝ : ℕ
⊢ drop x✝ (drop (n✝ + 1) []) = drop (x✝ + (n✝ + 1)) []
Tactic:
simp [drop]
State after:
no goals

State before:
α : Type
m n : ℕ
head✝ : α
xs : List α
⊢ drop n (drop (m + 1) (head✝ :: xs)) = drop (n + (m + 1)) (head✝ :: xs)
Tactic:
simp [drop, drop_drop m n xs, ← add_assoc]
State after:
no goals