proposition: Lemma zc0: z2Z c0 = 0.
proof: Proof. unfold z2Z, c0, z2Z; simpl. generalize ZnZ.spec_0; auto. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod