proposition: Lemma size_cyclotomic z n : size (cyclotomic z n) = (totient n).+1.
proof: Proof. rewrite /cyclotomic -big_filter size_prod_XsubC; congr _.+1. case: big_enumP => _ _ _ [_ ->]. rewrite totient_count_coprime -big_mkcond big_mkord -sum1_card. by apply: eq_bigl => k; rewrite coprime_sym. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly finset fingroup finalg zmodp cyclic) mathcomp(ssrnum ssrint archimedean polydiv intdiv mxpoly) mathcomp(rat vector falgebra fieldext separable galois algC)