proposition: Lemma QX_to_monic_spec : forall p : QX, p [#] [0] -> monic (QX_deg p) (QX_to_monic p).
proof: Proof. intros p H. apply QX_normalize_spec. assumption. Qed.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg