proposition: Lemma reduce_amd_aux_le n t1 t2 res : ([t1] < Zpower_nat wB n -> [t2] < [M] -> [res] < 2 * [M] - 1 -> [reduce_amd_aux_num n t1 t2 res] < 2 * [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; intros H1t1 Ht2 Hres. assert (H2t1 := to_Z_pos t1). rewrite add_correct, prod_correct. replace [t1] with 0%Z; auto with zarith. destruct t1 as [ | a t3]. intros _ Ht2 Hres. apply reduce_aux_le. apply Z.lt_le_trans with (1 := Hres). apply Z.le_trans with (2 * [M])%Z; auto with zarith. rewrite Zmult_comm. apply Zmult_le_compat_l. apply Z.le_trans with wB; try (red; discriminate). rewrite <- (Zmult_1_r wB) at 1; rewrite Zpower_nat_S. apply Zmult_le_compat_l. generalize (Zpower_base_pos n1); auto with zarith. red; discriminate. apply Zlt_le_weak; apply M_pos. nrom; intros Ht3 Ht2 Hres. 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. apply Hrec; auto with zarith. apply Zmult_lt_reg_r with wB; auto with zarith; try (red; auto; fail). repeat rewrite <- (Zmult_comm wB); apply Z.le_lt_trans with (2 := Ht3). case (to_Z_bounded a); auto with zarith. nrom; generalize M_pos; auto with zarith. apply Hrec; auto with zarith. apply Zmult_lt_reg_r with wB; auto with zarith; try (red; auto; fail). repeat rewrite <- (Zmult_comm wB); apply Z.le_lt_trans with (2 := Ht3). case (to_Z_bounded a); auto with zarith. rewrite shift_correct, add_correct, scal_correct; nrom. rewrite Hv. apply Zdiv_lt_upper_bound; try (red; auto; fail); auto with zarith. repeat apply Zplus_le_0_compat; repeat apply Zmult_le_0_compat; try apply to_Z_pos; try (red; discriminate). case (to_Z_bounded a); nrom; intros H1a H2a. case (to_Z_bounded (b * m')); nrom; intros H1bm H2bm. apply Z.le_lt_trans with (((2 * [M] - 2) + (wB - 1) * ([M] - 1) + (wB - 1) * [M])%Z). repeat apply Zplus_le_compat; auto with zarith. apply Zmult_le_compat; auto with zarith. apply to_Z_pos. apply Zmult_le_compat; auto with zarith. apply Zlt_le_weak; apply M_pos. ring_simplify; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63