proposition: Theorem in_ZPGroup: forall p, rel_prime p n -> 0 <= p < n -> In p ZPGroup.(s).
proof: Proof. intros p H (H1, H2); unfold ZPGroup; simpl. apply isupport_is_in. generalize (rel_prime_is_inv p); case (rel_prime_dec p); auto. apply mkZp_in; auto with zarith. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression