proposition: Theorem in_mkZp: forall p, In p mkZp -> 0 <= p < n.
proof: Proof. intros p H; case (in_mkZp_aux (Z.abs_nat (n - 1)) p). auto with zarith. 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