proposition: Lemma bv_mult_size: forall n a b, (size a) = n -> (@size b) = n -> size (bv_mult a b) = n.
proof: Proof. intros n a b H0 H1. unfold bv_mult, size, bits in *. rewrite H0, H1. rewrite N.eqb_compare. rewrite N.compare_refl. unfold mult_list, bvmult_bool. case_eq (length a). intros. + rewrite empty_list_length in H. rewrite H in *. now simpl in *. + intros. case n0 in *. now rewrite and_with_bool_len. rewrite prop_mult_bool_step. now rewrite and_with_bool_len. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance