theorem Std.Iter.drop_eq {α β : Type u_1} [Iterator α Id β] {n : Nat} {it : Iter β} : drop n it = (IterM.drop n it.toIterM).toIter

theorem Std.Iter.step_drop {α β : Type u_1} [Iterator α Id β] {n : Nat} {it : Iter β} : (drop n it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => match n with | 0 => PlausibleIterStep.yield (drop 0 it') out ⋯ | k.succ => PlausibleIterStep.skip (drop k it') ⋯ | ⟨IterStep.skip it', h⟩ => PlausibleIterStep.skip (drop n it') ⋯ | ⟨IterStep.done, h⟩ => PlausibleIterStep.done ⋯

theorem Std.Iter.atIdxSlow?_drop {α β : Type u_1} [Iterator α Id β] [Iterators.Productive α Id] {k l : Nat} {it : Iter β} : atIdxSlow? l (drop k it) = atIdxSlow? (l + k) it

@[simp]

theorem Std.Iter.toList_drop {α β : Type u_1} [Iterator α Id β] {n : Nat} [Iterators.Finite α Id] {it : Iter β} : (drop n it).toList = List.drop n it.toList

@[simp]

theorem Std.Iter.toListRev_drop {α β : Type u_1} [Iterator α Id β] {n : Nat} [Iterators.Finite α Id] {it : Iter β} : (drop n it).toListRev = List.take (it.toList.length - n) it.toList.reverse

@[simp]

theorem Std.Iter.toArray_drop {α β : Type u_1} [Iterator α Id β] {n : Nat} [Iterators.Finite α Id] {it : Iter β} : (drop n it).toArray = it.toArray.extract n