fact: Fixpoint mult_shift (a b: list _lit) (n: nat) : list carry := match a with | nil => mkzeros n | ai :: a' => (bblast_bvadd (and_with_bit b ai) (mult_shift a' (Lit._false :: b) n) (Clit Lit._false)) end.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance