rw [Nat.sub_add_cancel (Nat.sub_pos_of_lt (toNat_lt a))]
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ 2 ^ length α - (2 ^ length α - toNat a - 1 + 1) = 2 ^ length α - (2 ^ length α - toNat a)
no goals