Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
bn : Bool
n' : FinInt sz
bm : Bool
m' : FinInt sz
h :
  toSint (addfull (next bn n') (next bm m')) =
    match next bn n', next bm m' with
    | next false n'_1, next false m'_1 => toSint (next bn n') + toSint (next bm m')
    | next false n'_1, next true m'_1 =>
      match addfull (next bn n') (next bm m') with
      | next false a => toSint (next bn n') + toSint (next bm m') + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint (next bm m') - 2 ^ (sz + 1)
    | next true n'_1, next false m'_1 =>
      match addfull (next bn n') (next bm m') with
      | next false a => toSint (next bn n') + toSint (next bm m') + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint (next bm m') - 2 ^ (sz + 1)
    | next true n'_1, next true m'_1 => toSint (next bn n') + toSint (next bm m')
⊢ toSint (next bn n' + next bm m') =
    match next bn n', next bm m' with
    | next false n'_1, next false m'_1 =>
      match next bn n' + next bm m' with
      | next false a => toSint (next bn n') + toSint (next bm m')
      | next true a => toSint (next bn n') + toSint (next bm m') - 2 ^ (sz + 1)
    | next false n'_1, next true m'_1 => toSint (next bn n') + toSint (next bm m')
    | next true n'_1, next false m'_1 => toSint (next bn n') + toSint (next bm m')
    | next true n'_1, next true m'_1 =>
      match next bn n' + next bm m' with
      | next false a => toSint (next bn n') + toSint (next bm m') + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint (next bm m')
Tactic:
cases bn <;> cases bm <;> simp [addfull] at *
Proof state after:
case false.false
sz : ℕ
n' m' : FinInt sz
h :
  toSint
      (match addfull n' m' with
      | next false r => next false (next false r)
      | next true r => next false (next true r)) =
    toSint (next false n') + toSint (next false m')
⊢ toSint (next false n' + next false m') =
    match next false n' + next false m' with
    | next false a => toSint (next false n') + toSint (next false m')
    | next true a => toSint (next false n') + toSint (next false m') - 2 ^ (sz + 1)

case false.true
sz : ℕ
n' m' : FinInt sz
h :
  toSint
      (match addfull n' m' with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match addfull n' m' with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)
⊢ toSint (next false n' + next true m') = toSint (next false n') + toSint (next true m')

case true.false
sz : ℕ
n' m' : FinInt sz
h :
  toSint
      (match addfull n' m' with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match addfull n' m' with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)
⊢ toSint (next true n' + next false m') = toSint (next true n') + toSint (next false m')

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