∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] (it : Std.IterM Id α)
  (n : ℕ),
  Std.IterM.IsPlausibleNthOutputStep n it
    (match it.internalState.next.bind (Std.PRange.succMany? n) with
    | none => Std.IterStep.done
    | some next => Std.IterStep.yield { internalState := { next := Std.PRange.succ? next } } next)