fact: Definition bvmult_bool (a b: list bool) (n: nat) : list bool := let res := and_with_bool a (nth 0 b false) in match n with | O => res | S O => res | S (S k) => mult_bool_step a b res 1 k end.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance