List.drop of a positive

Stream: Is there code for X?

[Jakob von Raumer]

lemma drop_cons (xs : List α) (x : α) (h : 0 < i) : (x :: xs).drop i = xs.drop (i - 1) := by
  conv_lhs => rw [← Nat.sub_add_cancel (n := i) (m := 1) (by omega)]
  simp

We have the corresponding lemma for take but this seems to be missing? Or am I just unable to find it?

[Markus Himmel]

Yes, this seems to be missing.