fact: Fixpoint reduce_aux_num (n : nat) (t : number) := match n with | O => t | S n1 => match t with | nil => t | a :: _ => reduce_aux_num n1 (shift_num (add_num t (scal_num (a * m') M))) end end.
imports: List ZArith Znumtheory Uint63 Cyclic63