case succ sz ih =>
  simp [comp] at ih
  cases n; case next sz bn n' =>
  cases bn <;> simp [ih]
  . sorry_arith
  . sorry_arith
sz : ℕ
ih : ∀ (n : FinInt sz), toUint (comp n) = 2 ^ sz - 1 - toUint n
n : FinInt (Nat.succ sz)
⊢ toUint (comp n) = 2 ^ Nat.succ sz - 1 - toUint n
no goals