proposition: Lemma zx2qx_linear : forall c P, zx2qx (c[+X*]P) = (c:Q_as_CRing)[+X*]zx2qx P.
proof: Proof. reflexivity. Qed.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg