proposition: Lemma inj_Q_pres_plus : fun_pres_plus _ _ inj_Q_fun.
proof: Proof. intros x y; apply inj_Q_plus. Qed.
imports: CPoly_Degree CRing_Homomorphisms CoRN.model.ordfields.Qordfield CauchySeq Q_in_CReals CPoly_Euclid RingClass CRingClass Q_can nat_Q_lists RX_deg RX_div QX_root_loc