proposition: Theorem phi_divide_prime: forall n, 1 < n -> (n - 1 | phi n) -> prime n.
proof: Proof. intros n H1 H2; apply phi_n_minus_1_prime; auto. apply Zle_antisym. apply phi_le_n_minus_1; auto. apply Zdivide_le; auto; auto with zarith. apply phi_pos; auto. Qed.
imports: ZArith Znumtheory Tactic ZSum