proposition: Lemma sin_3PI2 : sin (3 * (PI / 2)) = -1.
proof: Proof. replace (3 * (PI / 2)) with (PI + PI / 2). - rewrite sin_plus; rewrite sin_PI; rewrite cos_PI; rewrite sin_PI2; ring. - pattern PI at 1; rewrite <-(Rplus_half_diag PI); ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt