no goals
α : Type u
β : Type v
γ : Type w
a : α
s : WSeq α
n : ℕ
⊢ drop (cons a s) (n + 1) = drop s n
induction n with
| zero => simp [drop]
| succ n n_ih =>
  simp [drop, ←n_ih]
no goals
case zero
α : Type u
β : Type v
γ : Type w
a : α
s : WSeq α
⊢ drop (cons a s) (Nat.zero + 1) = drop s Nat.zero
simp [drop]
no goals
case succ
α : Type u
β : Type v
γ : Type w
a : α
s : WSeq α
n : ℕ
n_ih : drop (cons a s) (n + 1) = drop s n
⊢ drop (cons a s) (Nat.succ n + 1) = drop s (Nat.succ n)
simp [drop, ←n_ih]