proposition: Lemma prop_mult_step3: forall k' a b res k, length (mult_step a b res k k') = (length res)%nat.
proof: Proof. intro k'. induction k'. - intros. simpl. rewrite prop_mult_step_k_h_len. simpl. lia. - intros. simpl. rewrite IHk'. rewrite prop_mult_step_k_h_len. simpl; lia. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance