proposition: Lemma is_iexp_fin_div (F : finFieldType) k s n p : p \in [char F] -> coprime p k -> (p %| n)%N -> is_iexp F k s n -> is_iexp F k s (n %/ p).
proof: Proof. move=> pC pCk pDn[nCk nI]; split => [|c cB]. by have := nCk; rewrite -{1}(divnK pDn) coprimeMl => /andP[]. apply: introspec_fin_div => //; first by rewrite coprime_sym. by apply: nI. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound