proposition: Theorem Zorder_power_is_1: forall p n, 1 < n -> rel_prime p n -> p ^ (Zorder p n) mod n = 1.
proof: Proof. intros p n H H1; unfold Zorder. case (Z_le_dec n 1); intros H2. contradict H; auto with zarith. let x := match goal with |- context[ZPGroup _ ?X] => X end in rewrite Zpower_mod_is_gpow with (Hn := x); auto with zarith. rewrite gpow_e_order_is_e. reflexivity. apply in_mod_ZPGroup; auto. apply Zlt_le_weak; apply e_order_pos. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression