proposition: Lemma reduce_bound_small t : (0 <= [t] < [M] -> 0 <= [reduce_num n t] < [M])%Z.
proof: Proof. intros Ht; apply reduce_bound. case Ht; intros _ Ht1; apply Z.lt_le_trans with (1 := Ht1). rewrite <-(Zmult_1_r [M]) at 1. apply Zmult_le_compat_l; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63