proposition: Lemma R_pi_as_IR : RasIR (PI) [=] Pi.
proof: Proof. assert (Sin (RasIR PI) [=] [0]). rewrite <- R_sin_as_IR. rewrite sin_PI. apply R_Zero_as_IR. assert (Not (forall z : Z, RasIR PI[#]zring (R:=IR) z[*]Pi)). unfold Not. intro X. apply ((eq_imp_not_ap _ _ _ H) (Sin_ap_Zero (RasIR (PI)) X)). clear H. apply (not_ap_imp_eq). intro PiNot. elim H0. intro z. elim z. simpl. rstepr ([0]:IR). stepr (RasIR 0); [| now apply R_Zero_as_IR]. apply R_ap_as_IR_back. apply PI_neq0. intro p. rewrite <- convert_is_POS. stepr (nring (R := IR) (nat_of_P p) [*] Pi); [| now apply mult_wdl; symmetry; apply (zring_plus_nat IR)]. case (nat_of_P p). simpl. rstepr ([0]:IR). stepr (RasIR 0); [| now apply R_Zero_as_IR]. apply R_ap_as_IR_back. apply PI_neq0. intro n. case n. simpl. rstepr (Pi). assumption. intro n0. apply less_imp_ap. apply leEq_less_trans with Four. rstepr (([1] [+] [1]) [*] ([1] [+] [1]):IR). rewrite <- R_One_as_IR. rewrite <- R_plus_as_IR. rewrite <- R_mult_as_IR. apply IR_le_as_R. apply PI_4. apply less_leEq_trans with (Two [*] Pi). rstepl (Two [*] Two:IR). apply mult_resp_less_lft. apply Pi_gt_2. rstepr (([0] [+] [1]) [+] [1] : IR). apply plus_one_ext_less. apply zero_lt_posplus1. apply eq_imp_leEq. reflexivity. apply mult_resp_leEq_rht. simpl. apply (plus_resp_leEq). apply (plus_resp_leEq). stepl (nring (R := IR) 0); [| now auto with *]. apply nring_leEq; auto with *. apply less_leEq. apply pos_Pi. intro p. apply Greater_imp_ap. simpl. apply leEq_less_trans with ([0]:IR). rewrite -> pring_convert. apply less_leEq. apply inv_cancel_less. rstepl ([0][*][0]:IR). rstepr ((nring (R:=IR) (nat_of_P p))[*]Pi). apply mult_resp_less_both. apply eq_imp_leEq. reflexivity. rstepl (nring (R := IR) 0) . apply nring_less. auto with *. apply eq_imp_leEq. reflexivity. auto with *. stepl (RasIR 0); [| now apply R_Zero_as_IR]. apply IR_lt_as_R. apply PI_RGT_0. 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)