proposition: Lemma qx2zx_spec : forall P, zx2qx (qx2zx P) [=] _C_ (Zlcm_den_poly P:Q_as_CRing) [*] P.
proof: Proof. intro P. unfold qx2zx. symmetry; apply zx2qx_spec. apply Zlcm_den_poly_spec. Qed.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg