simp [addv] at *
sz : ℕ
n m : FinInt (sz + 1)
h_nov : (addv n m).snd = false
⊢ toSint (addv n m).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
⊢ 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