proposition: Lemma check_bvmult_length2: forall bs1 bs2 bsres, check_mult bs1 bs2 bsres = true -> length bs1 = length bs2 .
proof: Proof. intros bs1. induction bs1. - intros. case bs2 in *. + easy. + unfold check_mult in H. now contradict H. - intros. unfold check_mult in H. case_eq (Nat.eqb (Datatypes.length (a :: bs1)) ((Datatypes.length bs2))). intros. now apply Nat.eqb_eq in H0. intros. rewrite H0 in H. now contradict H. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance