proposition: Lemma cos_PI2 : cos (PI / 2) = 0.
proof: Proof. unfold PI; generalize cos_pi2; replace ((2 * PI2)/2) with PI2 by field; tauto. 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