proposition: Theorem Zorder_div_power: forall p q n, 1 < n -> rel_prime p n -> p ^ q mod n = 1 -> (Zorder p n | q).
proof: Proof. intros p q n H H1 H2. assert (Hq: 0 <= q). generalize H2; case q; simpl; auto with zarith. intros p1 H3; contradict H3; rewrite Zmod_small; auto with zarith. unfold Zorder; case (Z_le_dec n 1). intros H3; contradict H; auto with zarith. intros H3; apply e_order_divide_gpow; auto. apply in_mod_ZPGroup; auto. rewrite <- Zpower_mod_is_gpow; auto with zarith. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression