proposition: Lemma cos_5PI4 : cos (5 * (PI / 4)) = -1 / sqrt 2.
proof: Proof. replace (5 * (PI / 4)) with (PI / 4 + PI) by field. rewrite neg_cos; rewrite cos_PI4; unfold Rdiv. ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt