theorem Std.Iterators.IterM.step_drop {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [Iterator α m β] {n : Nat} {it : IterM m β} : (drop n it).step = do let __do_lift ← it.step match __do_lift with | ⟨IterStep.yield it' out, h⟩ => match n with | 0 => pure (PlausibleIterStep.yield (drop 0 it') out ⋯) | k.succ => pure (PlausibleIterStep.skip (drop k it') ⋯) | ⟨IterStep.skip it', h⟩ => pure (PlausibleIterStep.skip (drop n it') ⋯) | ⟨IterStep.done, h⟩ => pure (PlausibleIterStep.done ⋯)