proposition: Lemma reduce_bound n t : ([t] < [M] * (Zpower_nat wB n) -> 0 <= [reduce_num n t] < [M])%Z.
proof: Proof. intros Ht; split. apply to_Z_pos. assert (HH := reduce_aux_le _ _ Ht). unfold reduce_num; case cp_spec; intros HH1; auto with zarith; rewrite sub_correct; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63