proposition: Lemma sin_3PI4 : sin (3 * (PI / 4)) = 1 / sqrt 2.
proof: Proof. replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field. now rewrite sin_shift, cos_neg, cos_PI4. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt