proposition: Lemma is_iexpm_totient R k s (M : {set 'Z_k}) : 1 < k -> Mk_spec R s M -> #|M| <= totient k.
proof: Proof. move:M; case: k => [|[|k /= M _ HM]] //. suff <-: #|[set i in 'I_k.+2 | coprime i k.+2]| = totient k.+2. apply/subset_leq_card/subsetP=> x; rewrite !inE; case: HM => // m -> []. by rewrite coprime_modl. rewrite -sum1_card big_mkcond /=. rewrite totient_count_coprime big_mkord. by apply: eq_bigr => i _; rewrite inE coprime_sym. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound