fact: Fixpoint mult_step (a b: list _lit) (res: list carry) (k k': nat) : list carry := let ak := List.firstn (S k') a in let b' := and_with_bit ak (nth k b Lit._false) in let res' := mult_step_k_h res b' (Clit Lit._false) (Z.of_nat k) in match k' with | O => res' | S pk' => mult_step a b res' (S k) pk' end.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance