proposition: Theorem in_mod_ZPGroup : forall (n : Z) (n_pos : 1 < n) (p : Z), rel_prime p n -> In (p mod n) (s (ZPGroup n n_pos)).
proof: Proof. intros n H p H1. apply in_ZPGroup; auto. apply rel_prime_mod; auto with zarith. apply Z_mod_lt; auto with zarith. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression