@[simp]

theorem String.Slice.Pos.le_find {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Pattern.SearchStep s)] [(s : Slice) → Std.Iterators.IteratorLoop (σ s) Id Id] {s : Slice} (pos : s.Pos) (pattern : ρ) [Pattern.ToForwardSearcher pattern σ] : pos ≤ pos.find pattern

@[simp]

theorem String.Pos.le_find {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.Iterators.IteratorLoop (σ s) Id Id] {s : String} (pos : s.Pos) (pattern : ρ) [Slice.Pattern.ToForwardSearcher pattern σ] : pos ≤ pos.find pattern