proposition: Theorem Zpower_mod_is_gpow: forall p q n (Hn: 1 < n), rel_prime p n -> 0 <= q -> p ^ q mod n = gpow (p mod n) (ZPGroup n Hn) q.
proof: Proof. intros p q n H Hp H1; generalize H1; pattern q; apply natlike_ind; simpl; auto. intros _; apply Zmod_small; auto with zarith. intros n1 Hn1 Rec _; simpl. generalize (in_mod_ZPGroup _ H _ Hp); intros Hu. unfold Z.succ; rewrite Zpower_exp; try rewrite Zpower_1_r; auto with zarith. rewrite gpow_add; auto with zarith. rewrite gpow_1; auto; rewrite <- Rec; auto. rewrite Zmult_mod; auto. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression