induction as generalizing n with
| nil => absurd hn; exact Nat.not_lt_zero n
| cons a as ih =>
  match n with
  | 0 =>
    rw [drop_succ_cons]
    rw [drop]
    rw [getElem_eq_get]
    rw [get]
    rw [drop]
  | n+1 =>
    rw [drop_succ_cons]
    rw [drop_succ_cons]
    rw [getElem_eq_get]
    rw [get_cons_succ]
    rw [←getElem_eq_get]
    exact ih ..
α : Type u_1
as : List α
n : Nat
hn : n < as.length
⊢ drop n as = as[n] :: drop (n + 1) as
no goals