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