c : Char
cs : List Char
i p : Pos
h : p ≠ 0
⊢ (ite (i + c = p) i (utf8PrevAux cs (i + c) p)).byteIdx < p.byteIdx
c : Char
cs : List Char
i p : Pos
h : p ≠ 0
⊢ (utf8PrevAux (c :: cs) i p).byteIdx < p.byteIdx
simp [utf8PrevAux]
case hneg
c : Char
cs : List Char
i p : Pos
h : p ≠ 0
h' : ¬i + c = p
⊢ (utf8PrevAux cs (i + c) p).byteIdx < p.byteIdx
case hpos
c : Char
cs : List Char
i p : Pos
h : p ≠ 0
h' : i + c = p
⊢ i.byteIdx < p.byteIdx

case hneg
c : Char
cs : List Char
i p : Pos
h : p ≠ 0
h' : ¬i + c = p
⊢ (utf8PrevAux cs (i + c) p).byteIdx < p.byteIdx
next => exact h' ▸ Nat.add_lt_add_left (one_le_csize _) _
no goals
case hneg
c : Char
cs : List Char
i p : Pos
h : p ≠ 0
h' : ¬i + c = p
⊢ (utf8PrevAux cs (i + c) p).byteIdx < p.byteIdx
next => exact utf8PrevAux_lt_of_pos _ _ _ h
no goals
c : Char
cs : List Char
i p : Pos
h : p ≠ 0
h' : i + c = p
⊢ i.byteIdx < p.byteIdx
exact h' ▸ Nat.add_lt_add_left (one_le_csize _) _
no goals
c : Char
cs : List Char
i p : Pos
h : p ≠ 0
h' : ¬i + c = p
⊢ (utf8PrevAux cs (i + c) p).byteIdx < p.byteIdx
exact utf8PrevAux_lt_of_pos _ _ _ h