proposition: Lemma cos_3PI4 : cos (3 * (PI / 4)) = -1 / sqrt 2.
proof: Proof. replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field. rewrite cos_shift; rewrite sin_neg; rewrite sin_PI4. unfold Rdiv. ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt