simp [h]
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 false r
⊢ toUint r = toUint (addfull n' m')
no goals