simp [addv]
sz : ℕ
n m : FinInt (sz + 1)
⊢ addv n m = addv m n
sz : ℕ
n m : FinInt (sz + 1)
⊢ (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)) =
    match m, n with
    | next false n', next false m' =>
      match m + n with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match m + n with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (m + n, false)