rw [Nat.land_comm, Nat.land_exp2_sub_one, Nat.mod_eq_of_lt (UInt.toNat_lt x)]
case incl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ 2 ^ length α - 1 &&& toNat x = toNat x
no goals