cases dn <;> cases dm <;> simp [h] at *
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')
case false.false
sz : ℕ
n' m' : FinInt sz
h_nov :
  (match next false n' + next false m' with
      | next msb r' => (next msb r', msb)).snd =
    false
h : True
⊢ toSint
      (match next false n' + next false m' with
        | next msb r' => (next msb r', msb)).fst =
    toSint (next false n') + toSint (next false m')

case true.true
sz : ℕ
n' m' : FinInt sz
h_nov :
  (match next true n' + next true m' with
      | next msb r' => (next msb r', !msb)).snd =
    false
h : True
⊢ toSint
      (match next true n' + next true m' with
        | next msb r' => (next msb r', !msb)).fst =
    toSint (next true n') + toSint (next true m')