proposition: Lemma dvdp_geom (R : comRingType) n (p : {poly R}) : p - 1 \is monic -> rdvdp (p - 1) (p ^+ n.+1 - 1).
proof: Proof. move=> pM; rewrite poly_geom mulrC rdvdp_mull //. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)