proposition: Theorem mkZp_in: forall p, 0 <= p < n -> In p mkZp.
proof: Proof. intros p (H1, H2); unfold mkZp; apply mkZp_aux_in. 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