proposition: Lemma cos_3PI2 : cos (3 * (PI / 2)) = 0.
proof: Proof. replace (3 * (PI / 2)) with (PI + PI / 2). - rewrite cos_plus; rewrite sin_PI; rewrite cos_PI2; ring. - pattern PI at 1 in |- *; rewrite <-(Rplus_half_diag PI). 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