proposition: Lemma is_iexp_mul (R : comRingType) k s m1 m2 : is_iexp R k s m1 -> is_iexp R k s m2 -> is_iexp R k s (m1 * m2).
proof: Proof. move=> [m1Ck Hm1] [m2Ck Hm2]; split; first by rewrite coprimeMl m1Ck. by move=> c Hc; apply: introspecMl; [apply: Hm1 | apply: Hm2]. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound