@[simp]

theorem String.utf8Size.go_append (cs₁ cs₂ : List Char) : utf8ByteSize.go (cs₁ ++ cs₂) = utf8ByteSize.go cs₁ + utf8ByteSize.go cs₂

@[simp]

theorem String.utf8Size.go_nil : utf8ByteSize.go [] = 0

@[simp]

theorem String.utf8Size.go_cons (c : Char) (cs : List Char) : utf8ByteSize.go (c :: cs) = utf8ByteSize.go cs + c.utf8Size

theorem String.next_le_endPosAux (p : Pos) (cs : List Char) (i ep : Pos) (lt : p < ep) (hep : ep = i + { byteIdx := utf8ByteSize.go cs }) : p + utf8GetAux cs i p ≤ ep

theorem String.next_le_endPos (s : String) (p : Pos) (lt : p < s.endPos) : s.next p ≤ s.endPos

theorem String.Iterator.next'_eq_next (it : Iterator) (h : it.hasNext = true) : it.next' h = it.next

theorem String.Iterator.next_toString (it : Iterator) : it.next.toString = it.toString

theorem String.Iterator.next_le_endPos (it : Iterator) (h : it.hasNext = true) : (it.next' h).pos ≤ (it.next' h).toString.endPos

theorem String.Iterator.lt_next (it : Iterator) : it.pos < it.next.pos

theorem String.Iterator.next_le_four (it : Iterator) : it.next.pos ≤ it.pos + { byteIdx := 4 }

@[simp]

theorem String.Iterator.next'_remainingBytes_lt {it : Iterator} {h : it.hasNext = true} : (it.next' h).remainingBytes < it.remainingBytes

theorem String.Iterator.curr'_eq_curr {it : Iterator} {h : it.hasNext = true} : it.curr' h = it.curr