. simp [h']; sorry_arith
case false
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next false r
h' : toUint r = toUint n' + toUint m'
⊢ 2 ^ sz + toUint r = toUint n' + (toUint m' - 2 ^ sz) + 2 ^ (sz + 1)

case true
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next true r
h' : 2 ^ sz + toUint r = toUint n' + toUint m'
⊢ toUint r = toUint n' + (toUint m' - 2 ^ sz)
case true
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next true r
h' : 2 ^ sz + toUint r = toUint n' + toUint m'
⊢ toUint r = toUint n' + (toUint m' - 2 ^ sz)