case next carry r =>
  have h₂: (addfull n m).toUint = (next carry r).toUint := by simp [h₁]
  cases carry <;> simp at h₂
  . simp [←h₂, FinInt.addfull_toUint, HAdd.hAdd]
  . simp [FinInt.addfull_toUint] at h₂
    rw [h₂] at h_bound
    sorry_arith
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
carry : Bool
r : FinInt sz
h₁ : addfull n m = next carry r
⊢ toUint
      (match next carry r with
      | next carry n => n) =
    Add.add (toUint n) (toUint m)
no goals