proposition: Lemma is_iexpm_order (R : comRingType) k s (M : {set 'Z_k}) n : 1 < k -> Mk_spec R s M -> is_iexp R k s n -> order_modn k n <= #|M|.
proof: Proof. move=> k_gt1 HMk nIN. have kCn : coprime k n by case: nIN; rewrite coprime_sym. rewrite order_modnE //; case: insubP => //= u nE uE. rewrite -[#[_]%g](card_imset _ val_inj). apply/subset_leq_card/subsetP => y /imsetP[z /cycleP[i ->] ->]. rewrite FinRing.val_unitX /= uE. apply: is_iexpm_X (HMk) _ => //. case: HMk => // /(_ _ nIN) /eqP[] /=. by rewrite -val_Zp_nat. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound