proposition: Lemma Cos_double_angle : forall x, (Cos(Two[*]x)[=][1][-]Two[*]Sin x[^]2).
proof: Proof. intros x. csetoid_replace (Two[*]x) (x[+]x);[|rational]. csetoid_rewrite (Cos_plus x x). set (sx:=Sin x). set (cx:=Cos x). rstepl ((cx[^]2)[-](sx[^]2)). unfold cg_minus. csetoid_replace (cx[^]2) ([1][-]sx[^]2). rational. apply cg_inv_unique_2. rstepl ((cx[^]2[+]sx[^]2)[-][1]). apply x_minus_x. apply FFT. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRArith CoRN.reals.fast.CRsin CoRN.reals.fast.CRpi CoRN.reals.fast.CRIR CoRN.reals.fast.Compress Coq.QArith.Qpower CoRN.model.ordfields.Qordfield Coq.QArith.Qround CoRN.transc.Pi CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.ContinuousCorrect CoRN.model.metric2.Qmetric CoRN.transc.SinCos CoRN.tactics.CornTac MathClasses.interfaces.abstract_algebra