fact: Definition reduce_mult_num (n: nat) (t1 t2 : number) := let res := reduce_amd_aux_num n t1 t2 nil in match cp_num res M with | Lt => res | _ => sub_num res M end.
imports: List ZArith Znumtheory Uint63 Cyclic63