proposition: Lemma z2ZN: z2Z zN = exx.(vN).
proof: Proof. apply (@ZnZ.of_Z_correct _ _ op_spec exx.(vN)); split; auto with zarith. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod