simp [comp] at ih
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
sz : ℕ
ih : ∀ (n : FinInt sz), toUint (logic1 (fun x => !x) n) = 2 ^ sz - 1 - toUint n
n : FinInt (Nat.succ sz)
⊢ toUint (comp n) = 2 ^ Nat.succ sz - 1 - toUint n