theorem
Std.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.inflate with
| ⟨IterStep.yield it' out, h⟩ =>
match n with
| 0 => pure (Shrink.deflate (PlausibleIterStep.yield (drop 0 it') out ⋯))
| k.succ => pure (Shrink.deflate (PlausibleIterStep.skip (drop k it') ⋯))
| ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (drop n it') ⋯))
| ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))