proposition: Lemma is_iexpm_mul (R : comRingType) k s (M : {set 'Z_k}) x y : 1 < k -> Mk_spec R s M -> x \in M -> y \in M -> (x * y) \in M.
proof: Proof. move=> k_gt1 MS. (do 3 case: (MS) => //) => Hm m1 yE m1I m xE mI _ _. have /eqP[] := Hm _ (is_iexp_mul mI m1I). by rewrite -modnMml -xE -modnMmr -yE /= {3}Zp_cast. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound