l r : List Char
it : Iterator
h : ValidFor l r it
⊢ utf8Len l = utf8Len l + utf8Len r ↔ r = []
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ it.i = endPos it.s ↔ r = []
simp [h.pos, h.toString, Pos.ext_iff]
no goals
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ utf8Len l = utf8Len l + utf8Len r ↔ r = []
exact (Nat.add_left_cancel_iff (m := 0)).trans <| eq_comm.trans utf8Len_eq_zero