proposition: Theorem Zorder_power_pos: forall p n, 1 < n -> rel_prime p n -> 0 < Zorder p n.
proof: Proof. intros p n H H1; unfold Zorder. case (Z_le_dec n 1); intros H2. contradict H; auto with zarith. apply e_order_pos. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression