proposition: Lemma sin_cos_PI4 : sin (PI / 4) = cos (PI / 4).
proof: Proof. rewrite cos_sin. replace (PI / 2 + PI / 4) with (- (PI / 4) + PI) by field. rewrite neg_sin, sin_neg; ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt