proposition: Theorem Zp_cyclic: prime n -> cyclic Z.eq_dec ZPGroup.
proof: Proof. intros H1. unfold ZPGroup, pmult; generalize (cyclic_field _ (fun x y => (x + y) mod n) (fun x y => (x * y) mod n) (fun x => (-x) mod n) 0); unfold IA; intros tmp; apply tmp; clear tmp; auto. intros; discriminate. apply mkZp_in; auto with zarith. intros; apply mkZp_in; auto with zarith. apply Z_mod_lt; auto with zarith. intros; rewrite Zplus_0_l; auto. apply Zmod_small; auto. apply in_mkZp; auto. intros; rewrite Zplus_comm; auto. intros a b c Ha Hb Hc. pattern a at 1; rewrite <- (Zmod_small a n); auto with zarith. pattern c at 2; rewrite <- (Zmod_small c n); auto with zarith. repeat rewrite <- Zplus_mod; auto with zarith. eq_tac; auto with zarith. apply in_mkZp; auto. apply in_mkZp; auto. intros; eq_tac; auto with zarith. intros a b c Ha Hb Hc. pattern a at 1; rewrite <- (Zmod_small a n); auto with zarith. repeat rewrite <- Zmult_mod; auto with zarith. repeat rewrite <- Zplus_mod; auto with zarith. eq_tac; auto with zarith. apply in_mkZp; auto. intros; apply mkZp_in; apply Z_mod_lt; auto with zarith. intros a Ha. pattern a at 1; rewrite <- (Zmod_small a n); auto with zarith. repeat rewrite <- Zplus_mod; auto with zarith. rewrite <- (Zmod_small 0 n); auto with zarith. eq_tac; auto with zarith. apply in_mkZp; auto. intros a b Ha Hb H; case (prime_mult n H1 a b). apply Zmod_divide; auto with zarith. intros H2; left. case (Zle_lt_or_eq 0 a); auto. case (in_mkZp a); auto. intros H3; absurd (n <= a). apply Zlt_not_le. case (in_mkZp a); auto. apply Zdivide_le; auto with zarith. intros H2; right. case (Zle_lt_or_eq 0 b); auto. case (in_mkZp b); auto. intros H3; absurd (n <= b). apply Zlt_not_le. case (in_mkZp b); auto. apply Zdivide_le; auto with zarith. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression