no goals
ι : Type ?u.206668
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
n : ℕ
h : n ≤ length l₁
⊢ drop n (l₁ ++ l₂) = drop n l₁ ++ l₂
simp [drop_append_eq_append_drop, tsub_eq_zero_iff_le.mpr h]