proposition: Lemma cos_pi2 : cos PI2 = 0.
proof: Proof. unfold PI2; case PI_2_aux; simpl. intros x [_ q]; rewrite <- (Ropp_involutive (cos x)), q; apply Ropp_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