proposition: Lemma is_iexp_X (R : comRingType) k s m n : is_iexp R k s m -> is_iexp R k s (m ^ n).
proof: Proof. move=> mI; elim: n => [|n IH]; first by apply: is_iexp1. by rewrite expnS; apply: is_iexp_mul. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound