proposition: Lemma cos2 : forall x:R, Rsqr (cos x) = 1 - Rsqr (sin x).
proof: Proof. intros x; rewrite <- (sin2_cos2 x); ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Rtrigo_def Rtrigo_alt Cos_rel Cos_plus ZArith_base Zcomplements Lia Lra Ranalysis1 Rsqrt_def PSeries_reg