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
⊢ Iterator.atEnd it = true ↔ r = []
simp [Iterator.atEnd, h.pos, h.toString]
no goals
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ utf8Len l ≥ utf8Len l + utf8Len r ↔ r = []
exact (Nat.add_le_add_iff_le_left _ _ 0).trans <| Nat.le_zero.trans utf8Len_eq_zero