fact: Fixpoint reduce_amd_aux_num (n : nat) (t1 t2 res : number) {struct n} := match n with | O => add_num res (prod_num t1 t2) | S n1 => match t1 with | nil => reduce_aux_num n res | a :: t3 => let res1 := add_num res (scal_num a t2) in match res1 with | nil => reduce_amd_aux_num n1 t3 t2 nil | b :: _ => reduce_amd_aux_num n1 t3 t2 (shift_num (add_num res1 (scal_num (b * m') M))) end end end.
imports: List ZArith Znumtheory Uint63 Cyclic63