case succ sz ih =>
  cases a; case next sz da a' =>
  cases b; case next db b' =>
  cases da <;> cases db <;> simp [toUint] at h <;> simp
  . apply ih _ _ h
  . have h₁ := @toUint_lt _ a'; have h₂ := @toUint_ge _ b'; sorry_arith
  . have h₁ := @toUint_ge _ a'; have h₂ := @toUint_lt _ b'; sorry_arith
  . apply ih; sorry_arith
sz : ℕ
ih : ∀ (a b : FinInt sz), toUint a = toUint b → a = b
a b : FinInt (Nat.succ sz)
h : toUint a = toUint b
⊢ a = b
no goals