proposition: Lemma sin_poly_fun_correct : forall (q:Q), inj_Q IR (sin_poly_fun q)[=]Three[*]inj_Q IR q[-]Four[*](inj_Q IR q[^]3).
proof: Proof. intros q. unfold sin_poly_fun. stepr (inj_Q IR (3*q-4*q^3)). apply inj_Q_wd. simpl; ring. rewrite inj_Q_minus. apply cg_minus_wd. stepr (inj_Q IR Three[*]inj_Q IR q). apply inj_Q_mult. apply mult_wdl. apply (inj_Q_nring IR 3). stepr (inj_Q IR Four[*]inj_Q IR (q^3)). apply inj_Q_mult. apply mult_wd. apply (inj_Q_nring IR 4). apply (inj_Q_power IR q 3). 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)