cases dn <;> cases dm <;> simp [FinInt.toUint, h', toSint]
<;> sorry_arith
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
n✝ : FinInt (sz + 0 + 1)
r : FinInt (sz + 0)
h : addfull n' m' = next true r
h' : toUint r = toUint n' + toUint m' - 2 ^ sz
⊢ toUint (next (dn || dm) (next (dn == dm) r)) = toUint (next dn n') + toUint (next dm m')
no goals