have h := add_toSint_msb n m
sz : ℕ
n m : FinInt (sz + 1)
h_nov :
  (match n, m with
      | next false n', next false m' =>
        match n + m with
        | next msb r' => (next msb r', msb)
      | next true n', next true m' =>
        match n + m with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (n + m, false)).snd =
    false
⊢ toSint
      (match n, m with
        | next false n', next false m' =>
          match n + m with
          | next msb r' => (next msb r', msb)
        | next true n', next true m' =>
          match n + m with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (n + m, false)).fst =
    toSint n + toSint m
sz : ℕ
n m : FinInt (sz + 1)
h_nov :
  (match n, m with
      | next false n', next false m' =>
        match n + m with
        | next msb r' => (next msb r', msb)
      | next true n', next true m' =>
        match n + m with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (n + m, false)).snd =
    false
h :
  toSint (n + m) =
    match n, m with
    | next false n', next false m' =>
      match n + m with
      | next false a => toSint n + toSint m
      | next true a => toSint n + toSint m - 2 ^ (sz + 1)
    | next false n', next true m' => toSint n + toSint m
    | next true n', next false m' => toSint n + toSint m
    | next true n', next true m' =>
      match n + m with
      | next false a => toSint n + toSint m + 2 ^ (sz + 1)
      | next true a => toSint n + toSint m
⊢ toSint
      (match n, m with
        | next false n', next false m' =>
          match n + m with
          | next msb r' => (next msb r', msb)
        | next true n', next true m' =>
          match n + m with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (n + m, false)).fst =
    toSint n + toSint m