proposition: Lemma rational_sin_small_correct : forall (a:Q) (Ha : -1 <= a <= 1), (@rational_sin_small a Ha == IRasCR (Sin (inj_Q IR a)))%CR.
proof: Proof. intros a Ha. unfold rational_sin_small. simpl. generalize (fun_series_conv_imp_conv (inj_Q IR a) (inj_Q IR a) (leEq_reflexive IR (inj_Q IR a)) sin_ps (sin_conv (inj_Q IR a) (inj_Q IR a) (leEq_reflexive IR (inj_Q IR a)) (compact_single_iprop realline (inj_Q IR a) I)) (inj_Q IR a) (compact_single_prop (inj_Q IR a)) (fun_series_inc_IR realline sin_ps sin_conv (inj_Q IR a) I)). intros H. rewrite <- (IR_inj_Q_as_CR a). rewrite (AltSeries_correct _ _ _ _ (sinStream_alt Ha) (sinStream_zl Ha) _ (AltSeries_convergent_0 _ _ _ _ (inj_Q IR a) (sinStream_alt Ha) (sinStream_zl Ha))). apply IRasCR_wd. - unfold series_sum. apply Lim_seq_eq_Lim_subseq with (fun n => 2*n)%nat. intros; lia. intros n; exists (S n); lia. intros n. induction n. apply eq_reflexive. replace (2*(S n))%nat with (S (S (2*n)))%nat by lia. set (n':=(2*n)%nat) in *. simpl in *. rstepr (seq_part_sum (fun n0 : nat => (sin_seq n0[/]nring (R:=IR) (fact n0)[//]nring_fac_ap_zero IR n0)[*] nexp IR n0 (inj_Q IR a[-][0])) n'[+]( (sin_seq n'[/]nring (R:=IR) (fact n')[//]nring_fac_ap_zero IR n')[*] nexp IR n' (inj_Q IR a[-][0])[+] (sin_seq (S n')[/]nring (R:=IR) (fact n' + n' * fact n')[//] nring_fac_ap_zero IR (S n'))[*] (nexp IR n' (inj_Q IR a[-][0])[*](inj_Q IR a[-][0])))). apply bin_op_wd_unfolded. assumption. rewrite <- cm_lft_unit. unfold sin_seq. apply bin_op_wd_unfolded. + destruct (even_or_odd_plus n') as [m [Hm|Hm]]; simpl. rational. elim (Nat.Even_Odd_False n'); [ exists n; subst n'; ring | now exists m; rewrite Hm, Nat.add_1_r; simpl; rewrite Nat.add_0_r]. + destruct (even_or_odd_plus (S n')) as [m [Hm|Hm]]; simpl. elim (Nat.Even_Odd_False (S n')). rewrite Hm. replace (m + m)%nat with (2*m)%nat by lia; now exists m. subst n'; exists n; ring. inversion Hm. unfold n' in H1. replace m with n by lia. clear Hm H1. transitivity (inj_Q IR ((1#Pos.of_nat (fact (1+2*n))) * ((-1)^n*a^(1+2*n))%Q)). clear IHn H. destruct n. simpl. apply inj_Q_wd. rewrite Qmult_1_l, Qmult_1_l. reflexivity. apply inj_Q_wd. rewrite Str_pth_sinStream. rewrite Nat2Pos.id. 2: discriminate. replace (Z.pos (Pos.of_nat (S n))) with (Z.of_nat (S n)). reflexivity. simpl. destruct n. reflexivity. rewrite <- Pos.succ_of_nat. reflexivity. discriminate. transitivity (inj_Q IR ((-(1))^n) [*] (inj_Q IR (a ^ (1 + 2 * n)) [*] inj_Q IR (1 # Pos.of_nat (fact (1 + 2 * n))))). rewrite <- inj_Q_mult, <- inj_Q_mult. apply inj_Q_wd. rewrite Qmult_comm. rewrite Qmult_assoc. reflexivity. change (inj_Q IR ((- (1)) ^ n) [*] (inj_Q IR (a ^ (1 + 2 * n)) [*] inj_Q IR (1 # Pos.of_nat (fact (1 + 2 * n)))) [=] (nexp IR n [--][1][/]nring (R:=IR) (fact (S n'))[//]nring_fac_ap_zero IR (S n'))[*] (nexp IR (S n') (inj_Q IR a[-][0]))). rstepr ((nexp IR n [--][1][*](nexp IR (S n') (inj_Q IR a[-][0])[/]nring (R:=IR) (fact (S n'))[//] nring_fac_ap_zero IR (S n')))). apply mult_wd. stepr ((inj_Q IR (-(1)))[^]n). apply inj_Q_power. apply nexp_wd. stepr ([--](inj_Q IR 1)). apply inj_Q_inv. apply un_op_wd_unfolded. rstepr (nring 1:IR). apply (inj_Q_nring IR 1). stepr (inj_Q IR ((1/P_of_succ_nat (pred (fact (1+2*n))))*a^(1+2*n)%nat)). rewrite <- inj_Q_mult. apply inj_Q_wd. rewrite Qmult_comm. apply Qmult_comp. replace (1 + 2 * Z.of_nat n)%Z with (Z.of_nat (1 + 2 * n)). reflexivity. rewrite <- (Nat2Z.inj_mul 2), <- (Nat2Z.inj_add 1). reflexivity. pose proof (fact_neq_0 (1+2*n)). destruct (fact (1+2*n)). exfalso; apply H0; reflexivity. simpl. destruct n0. reflexivity. rewrite <- Pos2SuccNat.id_succ, Nat2Pos.id. reflexivity. discriminate. rstepr ((nring 1[/]nring (R:=IR) (fact (S n'))[//] nring_fac_ap_zero IR (S n'))[*](nexp IR (S n') (inj_Q IR a[-][0]))). change (1+2*n)%nat with (S n'). stepr ((inj_Q IR (1 / Zpos (P_of_succ_nat (pred (fact (S n')))))[*](inj_Q IR (a^S n')))). apply inj_Q_mult. apply mult_wd. rewrite <- POS_anti_convert. assert (X:inj_Q IR (inject_Z (Z_of_nat (S (pred (fact (S n'))))))[#][0]). stepr (inj_Q IR [0]). assert (@cs_ap Q_as_CSetoid (inject_Z (Z_of_nat (S (pred (fact (S n')))))) 0). discriminate. destruct (ap_imp_less _ _ _ X). apply less_imp_ap. apply inj_Q_less. assumption. apply Greater_imp_ap. apply inj_Q_less. assumption. apply (inj_Q_nring IR 0). stepr ((inj_Q IR 1)[/](inj_Q IR (inject_Z (Z_of_nat (S (pred (fact (S n')))))))[//]X). apply inj_Q_div. apply div_wd. apply (inj_Q_nring IR 1). stepl (inj_Q IR (nring (fact (S n')))). apply inj_Q_nring. assert (Y:=lt_O_fact (S n')). apply inj_Q_wd. stepr ((fact (S n')):Q). clear - n'. induction (fact (S n')). simpl; reflexivity. rewrite inj_S. unfold Z.succ. simpl in *. rewrite -> IHn0. rewrite -> injz_plus. reflexivity. destruct (fact (S n')). exfalso; auto with *. simpl; reflexivity. stepr ((inj_Q IR a)[^](S n')). apply inj_Q_power. change (inj_Q IR a[^]S n'[=](inj_Q IR a[-][0])[^]S n'). apply nexp_wd. rational. - intro p. pose proof (Pos2Nat.is_pos p). destruct (Pos.to_nat p) eqn:des. exfalso; inversion H0. rewrite <- des. rewrite Pos2Nat.id. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRAlternatingSum_alg CoRN.reals.fast.CRstreams CoRN.reals.fast.CRexp CoRN.reals.fast.CRpi CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR Coq.QArith.Qpower Coq.QArith.Qabs CoRN.model.ordfields.Qordfield Coq.QArith.Qround CoRN.transc.Pi CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.ContinuousCorrect CoRN.model.metric2.Qmetric CoRN.transc.PowerSeries CoRN.transc.SinCos Coq.NArith.Ndigits CoRN.reals.fast.Compress CoRN.reals.fast.PowerBound CoRN.tactics.CornTac MathClasses.interfaces.abstract_algebra CoRN.util.Qdlog Coq(Lia)