theorem String.valid_prev {s : String} {p : Pos} (h : Pos.Valid s p) : Pos.Valid s (s.prev p)

theorem String.Pos.lt_def {a b : Pos} : a < b ↔ a.byteIdx < b.byteIdx

theorem String.Pos.sub_lt_sub_left {k m n : Pos} (h1 : k < m) (h2 : k < n) : m - n < m - k

theorem String.Pos.sizeof_lt_of_lt {a b : Pos} (h : a < b) : sizeOf a < sizeOf b