have h' := FinInt.addfull_toUint n' m'
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h : addfull n' m' = next br r
⊢ toSint
      (match next br r with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h : addfull n' m' = next br r
h' : toUint (addfull n' m') = toUint n' + toUint m'
⊢ toSint
      (match next br r with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')