proposition: Theorem phi_power_is_1: forall p n, 1 < n -> rel_prime p n -> p ^ (phi n) mod n = 1.
proof: Proof. intros p n H H1. assert (V1:= Zorder_power_pos p n H H1). assert (H2: (Zorder p n | phi n)). unfold Zorder. case (Z_le_dec n 1); intros H2. contradict H; auto with zarith. match goal with |- context[ZPGroup n ?H] => rewrite phi_is_order with (n_pos := H) end. apply e_order_divide_g_order. apply in_mod_ZPGroup; auto. case H2; clear H2; intros q H2; rewrite H2. rewrite Zmult_comm. assert (V2 := (phi_pos _ H)). assert (V3: 0 <= q). rewrite H2 in V2. apply Zlt_le_weak; apply Zmult_lt_0_reg_r with (2 := V2); auto with zarith. rewrite Zpower_mult; auto with zarith. rewrite Zpower_mod; auto with zarith. rewrite Zorder_power_is_1; auto. rewrite Zpower_1_l; auto with zarith. apply Zmod_small; auto with zarith. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression