case next dm m' =>
simp [addfull]
split
case h_1 r h =>
have h': r.toUint = n'.toUint + m'.toUint := by
rw [←ih n' m']; simp [h]
simp at h'
cases dn <;> cases dm <;> simp [FinInt.toUint, h']
<;> sorry_arith
case h_2 r h =>
have h': r.toUint = n'.toUint + m'.toUint - 2^sz := by
rw [←ih n' m']
simp [h, Int.add_comm, toSint]
simp at h'
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
⊢ toUint (addfull (next dn n') (next dm m')) = toUint (next dn n') + toUint (next dm m')
no goals