intros h_nov
sz : ℕ
n m : FinInt (sz + 1)
⊢ (addv n m).snd = false → toSint (addv n m).fst = toSint n + toSint m
sz : ℕ
n m : FinInt (sz + 1)
h_nov : (addv n m).snd = false
⊢ toSint (addv n m).fst = toSint n + toSint m