fact: Fixpoint mk_spec (w : univ_of_cycles) (op : ZnZ.Ops w) (op_spec : ZnZ.Specs op) (H: (1 < Zpos (ZnZ.digits op))%Z) (n : nat) {struct n} : ZnZ.Specs (mk_op op n) := match n return (ZnZ.Specs (mk_op op n)) with | O => op_spec | S n1 => @mk_zn2z_specs_karatsuba (word w n1) (mk_op op n1) (mk_spec op_spec H n1) end.
imports: CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) ZArith ZCAux Mod_op