proposition: Lemma reduce_amd_aux_correct n t1 t2 res : (([reduce_amd_aux_num n t1 t2 res] * Zpower_nat wB n) mod [M] = ([t1] * [t2] + [res]) mod [M])%Z.
proof: Proof. generalize t1 t2 res; clear t1 t2 res. induction n as [ |n1 Hrec]; intros t1 t2 res; unfold reduce_amd_aux_num; fold reduce_amd_aux_num. rewrite Zpower_nat_0, Zmult_1_r, add_correct, prod_correct, Zplus_comm; auto. destruct t1 as [ | a t3]; nrom. rewrite Zmult_0_l, Zplus_0_l, reduce_aux_correct; auto. set (v := add_num res (scal_num a t2)). assert (Hv: [v] = ([res] + to_Z a * [t2])%Z). unfold v; rewrite add_correct, scal_correct; auto. generalize Hv; destruct v as [ | b v1]; nrom; clear Hv; intros Hv. rewrite Zpower_nat_S, (Zmult_comm wB), Zmult_assoc, Zmult_mod, Hrec. nrom; rewrite Zplus_0_r, <- Zmult_mod. apply f_equal2 with (f := Z.modulo); auto. rewrite <- Zminus_0_r, Hv; ring. rewrite Zpower_nat_S, (Zmult_comm wB), Zmult_assoc, Zmult_mod, Hrec. rewrite <- Zmult_mod, shift_correct, add_correct, scal_correct; nrom. rewrite Zmult_plus_distr_l, reduce_aux_step. rewrite Zplus_assoc, Z_mod_plus_full. apply f_equal2 with (f := Z.modulo); auto. rewrite Hv; ring. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63