proposition: Lemma dvdpm_asym : antisymmetric dvdpm.
proof: Proof. move=> p q /andP [] /andP [] /andP [] Hp Hq Hpq /andP [] _ Hqp. by apply/eqP; rewrite -eqp_monic // /eqp Hpq. 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)