cases br <;> simp at *
sz : ℕ
n' m' : FinInt sz
h✝ : True
br : Bool
r : FinInt sz
h_nov :
  (match next br r with
      | next msb r' => (next msb r', !msb)).snd =
    false
h : next true n' + next true m' = next br r
⊢ toSint
      (match next br r with
        | next msb r' => (next msb r', !msb)).fst =
    toSint (next true n') + toSint (next true m')
case true
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next true n' + next true m' = next true r
h_nov : True
⊢ toSint (next true r) = toSint (next true n') + toSint (next true m')