proposition: Lemma reduce_mult_bound_small t1 t2 : (0 <= [t1] < [M] -> 0 <= [t2] < [M] -> 0 <= [reduce_mult_num n t1 t2] < [M])%Z.
proof: Proof. intros Ht1 Ht2; apply reduce_mult_bound; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63