simp [complement_eq, toNat_sub, toNat_add, toNat_zero]
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (~~~a) = 2 ^ length α - (toNat a + 1)
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ (2 ^ length α - (toNat a + toNat 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)