proposition: Lemma sin_poly_correct : forall x, AbsSmall (inj_Q IR (1)) x -> (IRasCR (Three[*]x[-]Four[*]x[^]3)==sin_poly (IRasCR x))%CR.
proof: Proof. intros x Hx. assert (Y:Continuous (clcr (inj_Q IR (-(1))) (inj_Q IR (1:Q))) ((Three:IR){**}FId{-}(Four:IR){**}FId{^}3)). eapply Derivative_imp_Continuous. apply DthreeXMinusFourX3. apply: (ContinuousCorrect (I:=(clcr (inj_Q IR (-(1))) (inj_Q IR (1:Q)))) (inj_Q_less _ (-1) 1 eq_refl) Y); [|repeat constructor|]. intros q Hq Hq0. transitivity (IRasCR (inj_Q IR (sin_poly_fun q)));[|apply IRasCR_wd; apply sin_poly_fun_correct]. simpl. change (' q)%CR with (Cunit_fun _ q). rewrite -> compress_fun_correct. rewrite -> Cmap_fun_correct. rewrite -> MonadLaw3. rewrite -> IR_inj_Q_as_CR. rewrite -> CReq_Qeq. simpl. unfold sin_poly_fun. setoid_replace (Qmax (- (1)) (Qmin 1 q)) with q. reflexivity. setoid_replace (Qmin 1 q) with q. rewrite <- Qle_max_r. apply leEq_inj_Q with IR. destruct Hq0; assumption. rewrite <- Qle_min_r. apply leEq_inj_Q with IR. destruct Hq0; assumption. destruct Hx; split;[stepl [--](inj_Q IR (1:Q)); [| now apply eq_symmetric; apply inj_Q_inv] |];assumption. 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)