proposition: Lemma dvd1pm (p : {poly T}) : p \is monic -> dvdpm 1 p.
proof: Proof. have H1:= (@monic1 T). move=> Hp; apply/andP; split; first by apply/andP. by rewrite dvd1p. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_fingroup) mathcomp(all_real_closed) CoqEAL(binetcauchy ssrcomplements mxstructure minor) CoqEAL(smith dvdring polydvd) CoqEAL(similar perm_eq_image companion closed_poly smith_complements)