cases n
sz : ℕ
n m : FinInt (sz + 1)
h :
  toSint (addfull n m) =
    match n, m with
    | next false n', next false m' => toSint n + toSint m
    | next false n', next true m' =>
      match addfull n m with
      | next false a => toSint n + toSint m + 2 ^ (sz + 1)
      | next true a => toSint n + toSint m - 2 ^ (sz + 1)
    | next true n', next false m' =>
      match addfull n m with
      | next false a => toSint n + toSint m + 2 ^ (sz + 1)
      | next true a => toSint n + toSint m - 2 ^ (sz + 1)
    | next true n', next true m' => toSint n + toSint m
⊢ 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
case next
sz : ℕ
m : FinInt (sz + 1)
a✝¹ : Bool
a✝ : FinInt sz
h :
  toSint (addfull (next a✝¹ a✝) m) =
    match next a✝¹ a✝, m with
    | next false n', next false m' => toSint (next a✝¹ a✝) + toSint m
    | next false n', next true m' =>
      match addfull (next a✝¹ a✝) m with
      | next false a => toSint (next a✝¹ a✝) + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next a✝¹ a✝) + toSint m - 2 ^ (sz + 1)
    | next true n', next false m' =>
      match addfull (next a✝¹ a✝) m with
      | next false a => toSint (next a✝¹ a✝) + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next a✝¹ a✝) + toSint m - 2 ^ (sz + 1)
    | next true n', next true m' => toSint (next a✝¹ a✝) + toSint m
⊢ toSint (next a✝¹ a✝ + m) =
    match next a✝¹ a✝, m with
    | next false n', next false m' =>
      match next a✝¹ a✝ + m with
      | next false a => toSint (next a✝¹ a✝) + toSint m
      | next true a => toSint (next a✝¹ a✝) + toSint m - 2 ^ (sz + 1)
    | next false n', next true m' => toSint (next a✝¹ a✝) + toSint m
    | next true n', next false m' => toSint (next a✝¹ a✝) + toSint m
    | next true n', next true m' =>
      match next a✝¹ a✝ + m with
      | next false a => toSint (next a✝¹ a✝) + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next a✝¹ a✝) + toSint m