proposition: Lemma prop_mult_step_k_h: forall a b c k, map interp_carry (mult_step_k_h a b c k) = RAWBITVECTOR_LIST.mult_bool_step_k_h (map interp_carry a) (map interp_carry b) (interp_carry c) k.
proof: Proof. intro a. induction a as [ | xa xsa IHa ]. - intros. case b. now simpl. intros. now simpl. - intros. case b in *. simpl. rewrite IHa. now simpl. intros. simpl. case (k - 1 <? 0)%Z. simpl. apply f_equal. apply IHa. rewrite <- map_cons. simpl. apply f_equal. apply IHa. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance