proposition: Theorem phi_n_minus_1_prime: forall n, 1 < n -> phi n = n - 1 -> prime n.
proof: Proof. intros n H H1; case (prime_dec n); auto; intros H2. assert (H3: phi n < n - 1); auto with zarith. replace (n-1) with ((1 + (n - 1) - 1) * 1); auto with zarith. assert (Hu: 1 <= n - 1); auto with zarith. rewrite <- Zsum_c; auto with zarith; unfold phi; apply Zsum_lt; auto. intros x _; case (rel_prime_dec x n); auto with zarith. case not_prime_divide with n; auto. intros x (H3, H4); exists x; repeat split; auto with zarith. case (rel_prime_dec x n); auto with zarith. intros H5; absurd (x = 1 \/ x = -1); auto with zarith. case (Zis_gcd_unique x n x 1); auto. apply Zis_gcd_intro; auto; exists 1; auto with zarith. contradict H3; rewrite H1; auto with zarith. Qed.
imports: ZArith Znumtheory Tactic ZSum