proposition: Theorem phi_is_length: phi n = Z_of_nat (length Lrel).
proof: Proof. assert (Hu: 0 < n); try apply Z.lt_trans with 1; auto with zarith. rewrite phi_def_with_0; auto. unfold Zsum, Lrel; rewrite Zle_imp_le_bool; auto with zarith. replace (1 + (n - 1) - 0) with n; auto with zarith. elim (progression Z.succ 0 (Z.abs_nat n)); simpl; auto. intros a l1 Rec. rewrite Rec. rewrite rel_prime_is_inv. case (rel_prime_dec a n); auto with zarith. simpl length; rewrite inj_S; auto with zarith. Qed.
imports: ZArith Znumtheory Zpow_facts Tactic Wf_nat UList FGroup EGroup IGroup Cyclic Euler ZProgression