proposition: Lemma QX_to_monic_apply : forall (p : QX) (a : Q), p ! a [=] [0] -> (QX_to_monic p) ! a [=] [0].
proof: Proof. intros p a Heq. unfold QX_to_monic; rewrite -> mult_apply; rewrite -> Heq; ring. Qed.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg