proposition: Lemma reduce_aux_le n t : ([t] < [M] * (Zpower_nat wB n) -> [reduce_aux_num n t] < 2 * [M])%Z .
proof: Proof. intros Ht. assert (HH: (exists U, [reduce_aux_num n t] * Zpower_nat wB n = [t] + U * [M] /\ 0 <= U < Zpower_nat wB n)%Z). generalize t; clear t Ht; induction n as [ | n Hrec]; intros t. assert (HM := to_Z_pos M). simpl reduce_aux_num; repeat rewrite Zpower_nat_0; repeat rewrite Zmult_1_r; auto with zarith. exists 0%Z; auto with zarith. repeat rewrite Zpower_nat_S. assert (HH2 := Zpower_base_pos n). simpl reduce_aux_num; case t; nrom. exists 0%Z; split. auto with zarith. split. auto with zarith. apply Zmult_lt_0_compat. 2: assumption. red; auto. intros a t1; nrom. case (Hrec (shift_num (add_num (a :: t1) (scal_num (a * m') M)))). intros U (H1U, H2U); exists (to_Z(a * m') + wB * U)%Z; split. rewrite (Zmult_comm wB), Zmult_assoc, H1U, shift_correct, add_correct, scal_correct; nrom. rewrite Zmult_plus_distr_l, reduce_aux_step; ring. case (to_Z_bounded (a * m')); nrom; intros H1am H2am. split. auto with zarith. apply Z.lt_le_trans with (wB + wB * U)%Z. auto with zarith. replace (wB * Zpower_nat wB n)%Z with (wB + wB * (Zpower_nat wB n - 1))%Z by ring; auto with zarith. apply Zmult_gt_0_lt_reg_r with (1 := Z.lt_gt _ _ (Zpower_base_pos n)). case HH; intros U (H1U, H2U). rewrite H1U. assert (U * [M] < [M] * Zpower_nat wB n)%Z. rewrite Zmult_comm; apply Zmult_gt_0_lt_compat_l. apply Z.lt_gt; apply M_pos. auto with zarith. replace (2 * [M] * Zpower_nat wB n)%Z with ([M] * Zpower_nat wB n + [M] * Zpower_nat wB n)%Z; auto with zarith; ring. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63