cs cs' : List Char
⊢ utf8Len cs + utf8Len cs' ≤ utf8Len cs ↔ cs' = []
cs cs' : List Char
⊢ atEnd { data := cs ++ cs' } { byteIdx := utf8Len cs } = true ↔ cs' = []
simp [atEnd_iff]
no goals
cs cs' : List Char
⊢ utf8Len cs + utf8Len cs' ≤ utf8Len cs ↔ cs' = []
cases cs' <;> simp [Pos.le_iff, Nat.lt_add_of_pos_right add_csize_pos]