theorem Std.Iter.atIdxSlow?_eq_match {α β : Type u_1} [Iterator α Id β] [Iterators.Productive α Id] {n : Nat} {it : Iter β} : atIdxSlow? n it = match it.step.val with | IterStep.yield it' out => match n with | 0 => some out | n.succ => atIdxSlow? n it' | IterStep.skip it' => atIdxSlow? n it' | IterStep.done => none