proposition: Theorem phi_is_order: phi n = g_order ZPGroup.
proof: Proof. unfold g_order; rewrite phi_is_length. eq_tac; apply permutation_length. apply ulist_incl2_permutation. unfold Lrel; apply isupport_aux_ulist. apply ulist_Zprogression; auto. apply ZPGroup.(unique_s). intros a H; unfold ZPGroup; simpl. apply isupport_is_in. unfold Lrel in H; apply isupport_aux_is_inv_true with (1 := H). apply mkZp_in; auto. assert (In a (progression Z.succ 0 (Z.abs_nat n))). apply (isupport_aux_incl _ pmult mkZp 1 Z.eq_dec); auto. split. apply Zprogression_le_init with (1 := H0). replace n with (0 + Z_of_nat (Z.abs_nat n)). apply Zprogression_le_end with (1 := H0). rewrite inj_Zabs_nat. rewrite Z.abs_eq; auto with zarith. intros a H; unfold Lrel; simpl. apply isupport_aux_is_in. simpl in H; apply isupport_is_inv_true with (1 := H). apply in_Zprogression. rewrite Zplus_0_l; rewrite inj_Zabs_nat; auto with zarith. rewrite Z.abs_eq; auto with zarith. assert (In a mkZp). apply (isupport_aux_incl _ pmult mkZp 1 Z.eq_dec); auto. apply in_mkZp; auto. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression