proposition: Lemma IZR_as_zring : forall x, IZR x = zring (R:=RRing) x.
proof: Proof. induction x. reflexivity. rewrite <- positive_nat_Z, <- INR_IZR_INZ. rewrite INR_as_nring. symmetry. rewrite positive_nat_Z. apply (pring_convert RRing p). change (IZR (Zneg p)) with (Ropp (IZR (Zpos p))). rewrite <- positive_nat_Z, <- INR_IZR_INZ. rewrite INR_as_nring. apply Ropp_eq_compat. symmetry. apply (pring_convert RRing p). Qed.
imports: Coq.QArith.QArith Coq.QArith.Qreals Coq.QArith.QArith_base CoRN.tactics.CornTac Coq.Reals.RIneq Coq.Reals.Rcomplete Coq.Reals.Rlimit Coq.Reals.Rbasic_fun CoRN.coq_reals.Rreals CoRN.reals.iso_CReals CoRN.reals.CauchySeq Coq.Reals.Rtrigo_def CoRN.transc.PowerSeries Coq.Logic.ConstructiveEpsilon Coq.Reals.Rlogic Coq.Reals.Reals CoRN.transc.Pi CoRN.transc.MoreArcTan CoRN.logic.PropDecid CoRN.transc.Exponential Coq(Lia Lra)