proposition: Lemma R_cos_as_IR : forall x, RasIR (cos x) [=] Cos (RasIR x).
proof: Proof. unfold cos. intro x. case (exist_cos (Rsqr x)). unfold cos_in. intros y rsums. rewrite -> (R_infsum_f_as_IR x y (fun x i => cos_n i * Rsqr x ^ i) rsums (R_infsum_as_IR_convergent _ _ rsums) ). simpl. unfold series_sum. apply Lim_seq_eq_Lim_subseq with (fun n => 2*n)%nat. intros; lia. intros n; exists (S n); lia. induction n. reflexivity. simpl in *. rewrite -> IHn. rewrite (Nat.add_comm n (S (n + 0))). simpl. rstepr ( seq_part_sum (fun n0 : nat => (cos_seq n0[/]nring (R:=IR) (fact n0)[//]nring_fac_ap_zero IR n0)[*] nexp IR n0 (RasIR x[-][0])) (n + 0 + n)[+] ( (cos_seq (n + 0 + n)[/]nring (R:=IR) (fact (n + 0 + n))[//] nring_fac_ap_zero IR (n + 0 + n))[*]nexp IR (n + 0 + n) (RasIR x[-][0])[+] (cos_seq (S (n + 0 + n))[/] nring (R:=IR) (fact (n + 0 + n) + (n + 0 + n) * fact (n + 0 + n))[//] nring_fac_ap_zero IR (S (n + 0 + n)))[*] (nexp IR (n + 0 + n) (RasIR x[-][0])[*](RasIR x[-][0]))) ). apply bin_op_wd_unfolded. rewrite Nat.add_comm. reflexivity. replace (n + 0 + n)%nat with (n + n)%nat by auto with *. unfold Rsqr. unfold cos_n. simpl. unfold cos_seq. simpl. destruct (even_or_odd_plus (n + n)). destruct (even_or_odd_plus (S(n + n))). simpl. destruct s; [ | exfalso; auto with *]. destruct s0; simpl. exfalso; auto with *. autorewrite with RtoIR. stepr ( (nexp IR x0 [--][1][/]nring (R:=IR) (fact (n + n))[//] nring_fac_ap_zero IR (n + n))[*]nexp IR (n + n) (RasIR x[-][0]) ). apply bin_op_wd_unfolded. replace (n + 0)%nat with n by auto with *. assert (Dom (f_rcpcl' IR) (RasIR (nring (R:=RRing) (fact (n + n))))). simpl. stepr (RasIR 0); [| now apply R_Zero_as_IR]. apply R_ap_as_IR_back. apply (nring_fac_ap_zero RReals (n + n)). rewrite -> (R_div_as_IR ((-1)^n) (nring (R := RRing) (fact (n + n))) X). apply div_wd. autorewrite with RtoIR. replace n with x0 by lia. reflexivity. autorewrite with RtoIR. reflexivity. clear. induction n; simpl. reflexivity. rewrite -> IHn. replace (n + S n)%nat with (S (n + n))%nat by auto with *. simpl. rstepr ( nexp IR (n + n) (RasIR x[-][0])[*]((RasIR x[-][0])[*](RasIR x[-][0])) ). apply bin_op_wd_unfolded. reflexivity. rational. setoid_replace (([0][/]nring (R:=IR) (fact (n + n) + (n + n) * fact (n + n))[//] nring_fac_ap_zero IR (S (n + n)))[*] (nexp IR (n + n) (RasIR x[-][0])[*](RasIR x[-][0]))) with ([0]:IR). rational. rational. 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)