proposition: Lemma reduce_correct n t : ([reduce_num n t] * (Zpower_nat wB n) mod [M] = [t] mod [M])%Z.
proof: Proof. assert (H:= M_pos). assert (HH:= reduce_aux_correct n t). unfold reduce_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