case succ sz ih =>
  cases n; case next sz dn n' =>
  cases m; 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 : ℕ
ih : ∀ (n m : FinInt sz), toUint (addfull n m) = toUint n + toUint m
n m : FinInt (Nat.succ sz)
⊢ toUint (addfull n m) = toUint n + toUint m
no goals