proposition: Lemma cos_PI4 : cos (PI / 4) = 1 / sqrt 2.
proof: Proof. Proof with trivial. apply Rsqr_inj... - apply cos_ge_0... + left; apply (Rlt_trans (- (PI / 2)) 0 (PI / 4) _PI2_RLT_0 PI4_RGT_0)... + left; apply PI4_RLT_PI2... - left; apply (Rmult_lt_0_compat 1 (/ sqrt 2))... + prove_sup... + apply Rinv_0_lt_compat; apply Rlt_sqrt2_0... - rewrite Rsqr_div'. rewrite Rsqr_1; rewrite Rsqr_sqrt... + unfold Rsqr; pattern (cos (PI / 4)) at 1; rewrite <- sin_cos_PI4; replace (sin (PI / 4) * cos (PI / 4)) with (1 / 2 * (2 * sin (PI / 4) * cos (PI / 4))) by field. rewrite <- sin_2a; replace (2 * (PI / 4)) with (PI / 2) by field. rewrite sin_PI2... field. + left; prove_sup... Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt