proposition: Lemma is_iexp_fin_char (F : finFieldType) k s p : p \in [char F] -> coprime p k -> is_iexp F k s p.
proof: Proof. by move=> pC pCk; split => // c _; apply: introspec_char. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound