proposition: Lemma monic_leadVMp (p : {poly R}) : (lead_coef p) \is a GRing.unit -> ((lead_coef p)^-1 *: p) \is monic.
proof: Proof. by move=> *; apply/monicP; rewrite lead_coefZ mulVr. Qed.
imports: mathcomp(all_ssreflect all_algebra)