cases m
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
m : FinInt (Nat.succ (Nat.add sz 0))
⊢ toUint (addfull (next dn n') m) = toUint (next dn n') + toUint m
case next
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
a✝¹ : Bool
a✝ : FinInt sz
⊢ toUint (addfull (next dn n') (next a✝¹ a✝)) = toUint (next dn n') + toUint (next a✝¹ a✝)