cs : List Char
c : Char
cs' : List Char
⊢ (if { byteIdx := utf8Len cs + csize c } = 0 then 0
    else utf8PrevAux (cs ++ c :: cs') 0 { byteIdx := utf8Len cs + csize c }) =
    { byteIdx := utf8Len cs }
cs : List Char
c : Char
cs' : List Char
⊢ prev { data := cs ++ c :: cs' } { byteIdx := utf8Len cs + csize c } = { byteIdx := utf8Len cs }
simp [prev]
cs : List Char
c : Char
cs' : List Char
⊢ utf8PrevAux (cs ++ c :: cs') 0 { byteIdx := utf8Len cs + csize c } = { byteIdx := utf8Len cs }
cs : List Char
c : Char
cs' : List Char
⊢ (if { byteIdx := utf8Len cs + csize c } = 0 then 0
    else utf8PrevAux (cs ++ c :: cs') 0 { byteIdx := utf8Len cs + csize c }) =
    { byteIdx := utf8Len cs }
refine (if_neg (Pos.ne_of_gt add_csize_pos)).trans ?_
no goals
cs : List Char
c : Char
cs' : List Char
⊢ utf8PrevAux (cs ++ c :: cs') 0 { byteIdx := utf8Len cs + csize c } = { byteIdx := utf8Len cs }
rw [utf8PrevAux_of_valid] <;> simp