proposition: Lemma inj_Q_pring : forall n, inj_Q (pring _ n) [=] pring R1 n.
proof: Proof. intros n. change (inj_Q (zring n)[=]zring n). stepr (inj_Q (nring n)). apply inj_Q_wd. rewrite <- inject_nat_convert. apply zring_plus_nat. stepr (nring n:R1). apply inj_Q_nring. apply eq_symmetric. rewrite <- inject_nat_convert. apply zring_plus_nat. Qed.
imports: CoRN.model.reals.Cauchy_IR CoRN.model.monoids.Nmonoid CoRN.model.rings.Zring CoRN.algebra.CRing_Homomorphisms CoRN.algebra.Expon Coq.QArith.Qpower CoRN.tactics.CornTac