proposition: Lemma reduce_mult_correct n t1 t2 : ([reduce_mult_num n t1 t2] * (Zpower_nat wB n) mod [M] = ([t1] * [t2]) mod [M])%Z.
proof: Proof. assert (H:= M_pos). generalize (reduce_amd_aux_correct n t1 t2 nil). nrom; rewrite Zplus_0_r; intros HH. unfold reduce_mult_num; case cp_spec; intros HH1; auto with zarith; rewrite sub_correct, Zmult_minus_distr_r; auto with zarith. rewrite (Zmult_comm [M]); unfold Zminus. rewrite Zopp_mult_distr_l, Z_mod_plus; auto with zarith. rewrite (Zmult_comm [M]); unfold Zminus. rewrite Zopp_mult_distr_l, Z_mod_plus; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63