proposition: Lemma rational_sin_bounded_correct_aux a : (sin_poly (IRasCR (Sin (inj_Q IR (a / 3)))) == IRasCR (Sin (inj_Q IR a)))%CR.
proof: Proof. rewrite <- sin_poly_correct; [|apply AbsIR_imp_AbsSmall; (stepr (nring 1:IR); [| now apply eq_symmetric; apply (inj_Q_nring IR 1)]); rstepr ([1]:IR); apply AbsIR_Sin_leEq_One]. apply IRasCR_wd. stepl (Sin (inj_Q IR (a/3*3))). apply Sin_wd. apply inj_Q_wd. simpl; field; discriminate. generalize (a/3). intros b; clear -b. stepr (Sin (Three[*](inj_Q IR b))). apply Sin_wd. stepr ((inj_Q IR b)[*](inj_Q IR (3:Q))). apply inj_Q_mult. csetoid_replace (inj_Q IR (3:Q)) (Three:IR). rational. apply (inj_Q_nring IR 3). apply Sin_triple_angle. 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)