proposition: Lemma prop_mult_step_k_h_len: forall a b c k, length (mult_step_k_h a b c k) = length a .
proof: Proof. intro a. induction a as [ | xa xsa IHa ]. - intros. simpl. easy. - intros. case b in *. simpl. rewrite IHa. simpl. lia. simpl. case (k - 1 <? 0)%Z; simpl; now rewrite 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