proposition: Lemma reduce_mult_bound n t1 t2 : ([t1] < Zpower_nat wB n -> [t2] < [M] -> 0 <= [reduce_mult_num n t1 t2] < [M])%Z.
proof: Proof. intros Ht1 Ht2; split. apply to_Z_pos. assert (Hres: ([nil] < 2 * [M] - 1)%Z). nrom; generalize M_pos; auto with zarith. assert (HH := reduce_amd_aux_le _ _ _ _ Ht1 Ht2 Hres). unfold reduce_mult_num; case cp_spec; intros HH1; auto with zarith; rewrite sub_correct; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63