proposition: Lemma R_sin_as_IR : forall x, RasIR (sin x) [=] Sin (RasIR x).
proof: Proof. unfold sin. intro x. case (exist_sin (Rsqr x)). unfold sin_in. intros y rsums. rewrite -> R_mult_as_IR. rewrite -> (R_infsum_f_as_IR x y (fun x i => sin_n i * Rsqr x ^ i) rsums (R_infsum_as_IR_convergent _ _ rsums) ). assert (convergent (fun n : nat => RasIR x[*](fun i : nat => RasIR (sin_n i * Rsqr x ^ i)) n)). apply conv_series_mult_scal. apply (R_infsum_as_IR_convergent _ _ rsums). rewrite <- (series_sum_mult_scal (fun i : nat => RasIR (sin_n i * Rsqr x ^ i)) (R_infsum_as_IR_convergent _ _ rsums) (RasIR x) X). 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. replace (n + 0 + n)%nat with (n + n)%nat by auto with *. unfold sin_n. simpl. replace (n + 0)%nat with (n)%nat by auto with *. unfold sin_seq at 3. unfold sin_seq at 3. simpl. destruct (even_or_odd_plus (n + n)). destruct (even_or_odd_plus (S(n + n))). destruct s; [ | exfalso; auto with *]. destruct s0; simpl. exfalso; auto with *. rstepr ( seq_part_sum (fun n0 : nat => (sin_seq n0[/]nring (R:=IR) (fact n0)[//]nring_fac_ap_zero IR n0)[*] nexp IR n0 (RasIR x[-][0])) (n + n)[+]( ([0][/]nring (R:=IR) (fact (n + n))[//]nring_fac_ap_zero IR (n + n))[*] nexp IR (n + n) (RasIR x[-][0])[+] (nexp IR x1 [--][1][/]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]))) ). apply bin_op_wd_unfolded. reflexivity. setoid_replace (RasIR x [-] [0]) with (RasIR x);[|rational]. replace x1 with n by lia. clear. setoid_replace (([0][/]nring (R:=IR) (fact (n + n))[//]nring_fac_ap_zero IR (n + n))[*] nexp IR (n + n) (RasIR x)) with ([0]:IR);[|rational]. rstepr ( RasIR x [*] ( (nexp IR n [--][1][/]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))) ). apply bin_op_wd_unfolded. reflexivity. autorewrite with RtoIR. unfold Rsqr. apply bin_op_wd_unfolded. cut (Dom (f_rcpcl' IR) (RasIR (nring (R:=RRing) (fact (n + n + 1))))). intro X. rewrite -> (R_div_as_IR ((-1)^n) (nring (R:=RRing) (fact (n + n + 1))) X). apply div_wd. autorewrite with RtoIR; reflexivity. autorewrite with RtoIR. apply nring_wd. replace (n + n + 1)%nat with (S (n + n)) by lia. simpl. reflexivity. simpl. stepr (RasIR 0); [| now apply R_Zero_as_IR]. apply R_ap_as_IR_back. apply (nring_fac_ap_zero RReals (n + n + 1)). induction n; simpl. reflexivity. replace (n + S n)%nat with (S(n + n)) by lia. simpl. rewrite -> IHn. autorewrite with RtoIR. 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)