cases br <;> simp [h₂] at *
sz : ℕ
n m : FinInt sz
br : Bool
r : FinInt sz
h : addfull n m = next br r
h₁ : toUint (next br r) = toUint n + toUint m
h₂ : n + m = r
⊢ toUint (n + m) =
    match next br r with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz
case false
sz : ℕ
n m r : FinInt sz
h : addfull n m = next false r
h₁ : toUint r = toUint n + toUint m
h₂ : True
⊢ toUint r = toUint n + toUint m

case true
sz : ℕ
n m r : FinInt sz
h : addfull n m = next true r
h₂ : True
h₁ : 2 ^ sz + toUint r = toUint n + toUint m
⊢ toUint r = toUint n + toUint m - 2 ^ sz