proposition: Lemma is_iexpm_X (R : comRingType) k s (M : {set 'Z_k}) x n : 1 < k -> Mk_spec R s M -> x \in M -> (x ^+ n) \in M.
proof: Proof. move=> k_gt1 MS xM. elim: n => [|n IH]; first by apply: is_iexpm1. by rewrite exprS; apply: is_iexpm_mul. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound