rw [Nat.succ_sub_succ_eq_sub]
α : Type u_1
n : Nat
x : α
xs : List α
h : n + 1 < length (x :: xs)
ih : length (drop n xs) = length xs - n
⊢ length (drop n xs) = length xs + 1 - (n + 1)
α : Type u_1
n : Nat
x : α
xs : List α
h : n + 1 < length (x :: xs)
ih : length (drop n xs) = length xs - n
⊢ length (drop n xs) = length xs - n