proposition: Lemma is_iexpm1 (R : comRingType) k s (M : {set 'Z_k}) : 1 < k -> Mk_spec R s M -> 1 \in M.
proof: Proof. move=> k_gt1 MS; case: MS => // /(_ 1%N (is_iexp1 _ _ _)). by rewrite modn_small ?eqxx. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound