proposition: Lemma is_power_exp p n : prime p -> is_power (p ^ n) p.
proof: Proof. by move=> pP; rewrite /is_power eqn_exp2l ?prime_gt1 // pfactorK. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)