proposition: Theorem phi_pos: forall n, 1 < n -> 0 < phi n.
proof: Proof. intros n H; unfold phi. case (Zle_lt_or_eq 2 n); auto with zarith; intros H1; subst. rewrite Zsum_S_left; simpl; auto with zarith. case (rel_prime_dec 1 n); intros H2. apply Z.lt_le_trans with (1 + 0); auto with zarith. apply Zplus_le_compat_l. pattern 0 at 1; replace 0 with ((1 + (n - 1) - 2) * 0); auto with zarith. rewrite <- Zsum_c; auto with zarith. apply Zsum_le; auto with zarith. intros x H3; case (rel_prime_dec x n); auto with zarith. case H2; apply rel_prime_1; auto with zarith. rewrite Zsum_nn. case (rel_prime_dec (2 - 1) 2); auto with zarith. intros H1; contradict H1; apply rel_prime_1; auto with zarith. Qed.
imports: ZArith Znumtheory Tactic ZSum