proposition: Lemma R_pi_alt_as_IR : RasIR (Alt_PI) [=] pi.
proof: Proof. unfold Alt_PI. unfold pi. destruct (exist_PI) as [x prf]. unfold pi_series. unfold tg_alt in prf. unfold PI_tg in prf. rewrite -> R_mult_as_IR. apply mult_wd. change 4 with ((1 + 1) * (1 + 1)). rewrite -> R_mult_as_IR. rewrite -> R_plus_as_IR. rewrite -> R_One_as_IR. rational. rewrite -> (R_infsum_as_IR x ( (fun i : nat => (-1) ^ i * / INR (2 * i + 1)) ) prf (R_infsum_as_IR_convergent _ _ prf) ). apply series_sum_wd. intro n. autorewrite with RtoIR. apply mult_wd. simpl; reflexivity. stepr (RasIR (1 / nring (R:=RRing) (2 * n + 1))). apply R_as_IR_wd. unfold Rdiv. simpl; auto with *. cut (n + (n + 0) + 1 = S (n + n))%nat. intro DF. cut (Dom (f_rcpcl' IR) (RasIR (nring (R:=RReals) (2 * n + 1)))). intro H. rewrite -> (R_recip_as_IR (nring (R:=RReals) (2 * n + 1)) H). apply div_wd. reflexivity. rewrite -> R_nring_as_IR. apply nring_wd. rewrite <- DF. simpl. auto. simpl. stepr (RasIR 0); [| now apply R_Zero_as_IR]. apply R_ap_as_IR_back. apply Rgt_not_eq. rewrite DF. unfold Rgt. change ([0] [<] nring (R:=RRing) (S (n + n))). apply pos_nring_S. auto with *. 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)