α : Type u
β : Type v
γ : Type w
s : WSeq α
n : ℕ
⊢ drop (tail s) n = drop s (1 + n)
α : Type u
β : Type v
γ : Type w
s : WSeq α
n : ℕ
⊢ drop (tail s) n = drop s (n + 1)
rw [add_comm]
α : Type u
β : Type v
γ : Type w
s : WSeq α
n : ℕ
⊢ drop s (1 + n) = drop (tail s) n
α : Type u
β : Type v
γ : Type w
s : WSeq α
n : ℕ
⊢ drop (tail s) n = drop s (1 + n)
symm
no goals
α : Type u
β : Type v
γ : Type w
s : WSeq α
n : ℕ
⊢ drop s (1 + n) = drop (tail s) n
apply dropn_add