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