cases bn <;> simp [ih]
sz : ℕ
bn : Bool
n' : FinInt sz
ih : ∀ (n : FinInt (Nat.add sz 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add sz 0 - 1 - toUint n
⊢ toUint (comp (next bn n')) = 2 ^ Nat.succ (Nat.add sz 0) - 1 - toUint (next bn n')
case false
sz : ℕ
n' : FinInt sz
ih : ∀ (n : FinInt (Nat.add sz 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add sz 0 - 1 - toUint n
⊢ 2 ^ sz + (2 ^ sz - 1 - toUint n') = 2 ^ Nat.succ sz - 1 - toUint n'

case true
sz : ℕ
n' : FinInt sz
ih : ∀ (n : FinInt (Nat.add sz 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add sz 0 - 1 - toUint n
⊢ 2 ^ sz - 1 - toUint n' = 2 ^ Nat.succ sz - 1 - (2 ^ sz + toUint n')