proposition: Theorem mkZp_length: length mkZp = Z.abs_nat n.
proof: Proof. unfold mkZp; rewrite mkZp_aux_length. apply inj_eq_rev. rewrite inj_plus. simpl; repeat rewrite inj_Zabs_nat. repeat rewrite Z.abs_eq; auto with zarith. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression