proposition: Lemma injZ_strext : fun_strext (inject_Z : Z_as_CRing -> Q_as_CRing).
proof: Proof. intros x y. unfold inject_Z; simpl; unfold Qap, Qeq, ap_Z; simpl. rewrite Zmult_1_r, Zmult_1_r; tauto. Qed.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg