simp [add_toSint_msb]
case false
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next false n' + next false m' = next false r
h_nov : True
⊢ toSint (next false n' + next false m') = toSint (next false n') + toSint (next false m')
case false
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next false n' + next false m' = next false r
h_nov : True
⊢ (match next false n' + next false m' with
    | next false a => toSint (next false n') + toSint (next false m')
    | next true a => toSint (next false n') + toSint (next false m') - 2 ^ (sz + 1)) =
    toSint (next false n') + toSint (next false m')