proposition: Theorem Zorder_div: forall p n, prime n -> ~(n | p) -> (Zorder p n | n - 1).
proof: Proof. intros p n H; unfold Zorder. case (Z_le_dec n 1); intros H1 H2. contradict H1; generalize (prime_ge_2 n H); auto with zarith. rewrite <- prime_phi_n_minus_1; auto. match goal with |- context[ZPGroup _ ?H2] => rewrite phi_is_order with (n_pos := H2) end. apply e_order_divide_g_order; auto. apply in_mod_ZPGroup; auto. apply rel_prime_sym; apply prime_rel_prime; auto. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression