fact: Definition znz_of_Z (w: univ_of_cycles) (op: ZnZ.Ops w) z := match z with | Zpos p => snd (ZnZ.of_pos p) | _ => ZnZ.zero end.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) ZCAux W Mod_op LucasLehmer Bits