rw [UInt.toNat_complement, Nat.add_comm, Nat.sub_add_eq]
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ Nat.getBit (toNat (~~~x)) i = (Nat.getBit (toNat x) i != decide (i < length α))
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ Nat.getBit (2 ^ length α - 1 - toNat x) i = (Nat.getBit (toNat x) i != decide (i < length α))