case next dm m' =>
cases dn <;> cases dm <;> simp [h] at *
case false.false =>
match h: next false n' + next false m' with
| .next br r =>
rw [h] at h_nov
cases br <;> simp at *
rw [←h]; simp [add_toSint_msb]; simp [h]
case true.true =>
match h: next true n' + next true m' with
| .next br r =>
rw [h] at h_nov
cases br <;> simp at *
rw [←h]; simp [add_toSint_msb]; simp [h]
sz : ℕ
dn : Bool
n' : FinInt sz
dm : Bool
m' : FinInt sz
h_nov :
  (match next dn n', next dm m' with
      | next false n'_1, next false m'_1 =>
        match next dn n' + next dm m' with
        | next msb r' => (next msb r', msb)
      | next true n'_1, next true m'_1 =>
        match next dn n' + next dm m' with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (next dn n' + next dm m', false)).snd =
    false
h :
  toSint (next dn n' + next dm m') =
    match next dn n', next dm m' with
    | next false n'_1, next false m'_1 =>
      match next dn n' + next dm m' with
      | next false a => toSint (next dn n') + toSint (next dm m')
      | next true a => toSint (next dn n') + toSint (next dm m') - 2 ^ (sz + 1)
    | next false n'_1, next true m'_1 => toSint (next dn n') + toSint (next dm m')
    | next true n'_1, next false m'_1 => toSint (next dn n') + toSint (next dm m')
    | next true n'_1, next true m'_1 =>
      match next dn n' + next dm m' with
      | next false a => toSint (next dn n') + toSint (next dm m') + 2 ^ (sz + 1)
      | next true a => toSint (next dn n') + toSint (next dm m')
⊢ toSint
      (match next dn n', next dm m' with
        | next false n'_1, next false m'_1 =>
          match next dn n' + next dm m' with
          | next msb r' => (next msb r', msb)
        | next true n'_1, next true m'_1 =>
          match next dn n' + next dm m' with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (next dn n' + next dm m', false)).fst =
    toSint (next dn n') + toSint (next dm m')
no goals