Documentation

Std.Data.Iterators.Lemmas.Combinators.DropWhile

theorem Std.Iterators.Iter.Intermediate.dropWhile_eq_dropWhile_toIterM {α β : Type u_1} [Iterator α Id β] {P : βBool} {it : Iter β} {dropping : Bool} :
dropWhile P dropping it = (IterM.Intermediate.dropWhile P dropping it.toIterM).toIter
theorem Std.Iterators.Iter.step_intermediateDropWhile {α β : Type u_1} [Iterator α Id β] {it : Iter β} {P : βBool} {dropping : Bool} :