proposition: Lemma is_power_id p : prime p -> is_power p p.
proof: Proof. by move=> pP; rewrite -{1}(expn1 p) is_power_exp. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)