cases br <;> simp
sz : ℕ
n m : FinInt sz
br : Bool
r' : FinInt sz
h_full : addfull n m = next br r'
⊢ (match next br r' with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz) =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz
case false
sz : ℕ
n m r' : FinInt sz
h_full : addfull n m = next false r'
⊢ toUint n + toUint m = if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz

case true
sz : ℕ
n m r' : FinInt sz
h_full : addfull n m = next true r'
⊢ toUint n + toUint m - 2 ^ sz =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz