n : ℕ
v : Bitvec n
⊢ Bitvec.toNat v < 2 ^ n
n : ℕ
v : Bitvec n
⊢ ↑(toFin v) = Bitvec.toNat v
rw [toFin, Fin.coe_ofNat_eq_mod, Nat.mod_eq_of_lt]
no goals
n : ℕ
v : Bitvec n
⊢ Bitvec.toNat v < 2 ^ n
apply toNat_lt