case zero
ι : Type ?u.491870
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
m : ℕ
xs : List α
⊢ dropSlice zero m xs = take zero xs ++ drop (zero + m) xs

case succ
ι : Type ?u.491870
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
m n✝ : ℕ
n_ih✝ : ∀ (xs : List α), dropSlice n✝ m xs = take n✝ xs ++ drop (n✝ + m) xs
xs : List α
⊢ dropSlice (succ n✝) m xs = take (succ n✝) xs ++ drop (succ n✝ + m) xs
ι : Type ?u.491870
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ xs : List α
n m : ℕ
⊢ dropSlice n m xs = take n xs ++ drop (n + m) xs
induction n generalizing xs
no goals
case zero
ι : Type ?u.491870
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
m : ℕ
xs : List α
⊢ dropSlice zero m xs = take zero xs ++ drop (zero + m) xs
cases xs <;> simp [dropSlice]
no goals
case succ
ι : Type ?u.491870
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
m n✝ : ℕ
n_ih✝ : ∀ (xs : List α), dropSlice n✝ m xs = take n✝ xs ++ drop (n✝ + m) xs
xs : List α
⊢ dropSlice (succ n✝) m xs = take (succ n✝) xs ++ drop (succ n✝ + m) xs
cases xs <;> simp [dropSlice, *, Nat.succ_add]