proposition: Theorem phi_def_with_0: forall n, 1< n -> phi n = Zsum 0 (n - 1) (fun x => if rel_prime_dec x n then 1 else 0).
proof: Proof. intros n H; rewrite Zsum_S_left; auto with zarith. case (rel_prime_dec 0 n); intros H2. contradict H2; apply not_rel_prime_0; auto. rewrite Zplus_0_l; auto. Qed.
imports: ZArith Znumtheory Tactic ZSum