proposition: Lemma sin2_cos2 : forall x:R, Rsqr (sin x) + Rsqr (cos x) = 1.
proof: Proof. intro; unfold Rsqr in |- *; rewrite Rplus_comm; rewrite <- (cos_minus x x); unfold Rminus in |- *; rewrite Rplus_opp_r; apply cos_0. 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