proposition: Lemma prime_is_power_exp p q n : prime p -> 1 < q -> 0 < n -> is_power (q ^ n) p -> is_power q p.
proof: Proof. move=> pP q_gt1 n_gt0. have q_gt0 : 0 < q by apply: ltnW. by rewrite /is_power lognX mulnC expnM eqn_exp2r. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)