s : String
i : Pos
h : i ≠ 0
⊢ (utf8PrevAux s.data 0 i).byteIdx < i.byteIdx
s : String
i : Pos
h : i ≠ 0
⊢ (prev s i).byteIdx < i.byteIdx
simp [prev, h]
no goals
s : String
i : Pos
h : i ≠ 0
⊢ (utf8PrevAux s.data 0 i).byteIdx < i.byteIdx
exact utf8PrevAux_lt_of_pos _ _ _ h