proposition: Lemma reduce_aux_correct n t : ([reduce_aux_num n t] * (Zpower_nat wB n) mod [M] = [t] mod [M])%Z.
proof: Proof. generalize t; clear t. induction n as [ | n Hrec]; intros t. assert (HH := to_Z_pos t). simpl reduce_aux_num; repeat rewrite Zpower_nat_0; repeat rewrite Zmult_1_r; auto. repeat rewrite Zpower_nat_S. simpl reduce_aux_num; case t. nrom; rewrite Zmod_small, Zmult_0_l; auto with zarith. rewrite Zmult_0_l; auto with zarith. generalize M_pos; auto with zarith. intros a t1. rewrite (Zmult_comm wB), Zmult_assoc, Zmult_mod, Hrec, <- Zmult_mod, shift_correct, add_correct, scal_correct. nrom. rewrite reduce_aux_step, Zplus_mod, Z_mod_mult, Zplus_0_r, Zmod_mod; auto. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63