proposition: Theorem prime_phi_n_minus_1: forall n, prime n -> phi n = n - 1.
proof: Proof. intros n H; replace (n-1) with ((1 + (n - 1) - 1) * 1); auto with zarith. assert (Hu: 1 <= n - 1). assert (2 <= n); auto with zarith. apply prime_ge_2; auto. rewrite <- Zsum_c; auto with zarith; unfold phi; apply Zsum_ext; auto. intros x (H2, H3); case H; clear H; intros H H1. generalize (H1 x); case (rel_prime_dec x n); auto with zarith. intros H6 H7; contradict H6; apply H7; split; auto with zarith. Qed.
imports: ZArith Znumtheory Tactic ZSum