n : ℕ
i j : Fin (2 ^ n)
h : i ≤ j
⊢ ↑i ≤ ↑j
n : ℕ
i j : Fin (2 ^ n)
h : i ≤ j
⊢ Bitvec.toNat (Bitvec.ofNat n ↑i) ≤ Bitvec.toNat (Bitvec.ofNat n ↑j)
simp only [toNat_ofNat, Nat.mod_eq_of_lt, Fin.is_lt]
no goals
n : ℕ
i j : Fin (2 ^ n)
h : i ≤ j
⊢ ↑i ≤ ↑j
exact h