proposition: Lemma injZ_pres_plus : fun_pres_plus _ _ injZ_fun.
proof: Proof. intros x y. simpl; unfold inject_Z, Qeq; simpl. ring. Qed.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg