remove obsolete todo

Author: datokrat

src/Std/Data/Iterators/Combinators/Drop.lean

@@ -27,8 +27,6 @@ it.drop 3   ------⊥
 * `Finite` instance: only if `it` is finite
 * `Productive` instance: only if `it` is productive
 
-_TODO_: prove `Productive`
-
 **Performance:**
 
 Currently, this combinator incurs an additional O(1) cost with each output of `it`, even when the iterator

src/Std/Data/Iterators/Combinators/Monadic/Drop.lean

@@ -46,8 +46,6 @@ it.drop 3   ------⊥
 * `Finite` instance: only if `it` is finite
 * `Productive` instance: only if `it` is productive
 
-_TODO_: prove `Productive`
-
 **Performance:**
 
 Currently, this combinator incurs an additional O(1) cost with each output of `it`, even when the iterator