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

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

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

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