simp [add_toSint_msb]
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 n' + next true m') = 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
⊢ (match next true n' + next true m' with
    | next false a => toSint (next true n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next true m')) =
    toSint (next true n') + toSint (next true m')