have h₂: n+m = r := by simp [HAdd.hAdd, add, h]
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
⊢ toUint (n + m) =
    match next br r with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz
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