n : ℕ
⊢ bitsToNat [decide (n % 2 = 1)] = n % 2
n : ℕ
⊢ Bitvec.toNat (decide (n % 2 = 1) ::ᵥ Vector.nil) = n % 2
simp [bitsToNat_toList]
n : ℕ
⊢ List.foldl (fun r b => r + r + bif b then 1 else 0) (0 + 0 + bif decide (n % 2 = 1) then 1 else 0) [] = n % 2
n : ℕ
⊢ bitsToNat [decide (n % 2 = 1)] = n % 2
unfold bitsToNat addLsb List.foldl
no goals
n : ℕ
⊢ List.foldl (fun r b => r + r + bif b then 1 else 0) (0 + 0 + bif decide (n % 2 = 1) then 1 else 0) [] = n % 2
simp [Nat.cond_decide_mod_two, -Bool.cond_decide]