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

theorem Std.Iterators.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.Iterators.Iter.atIdxSlow?_drop {α β : Type u_1} [Iterator α Id β] [Productive α Id] {k l : Nat} {it : Iter β} : atIdxSlow? l (drop k it) = atIdxSlow? (l + k) it

@[simp]

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

@[simp]

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

theorem Std.Iterators.List.drop_eq_extract {α : Type u_1} {l : List α} {k : Nat} : List.drop k l = l.extract k

@[simp]

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