proposition: Lemma cos_PI6 : cos (PI / 6) = sqrt 3 / 2.
proof: Proof. Proof with trivial. apply Rsqr_inj... - apply cos_ge_0... + left; apply (Rlt_trans (- (PI / 2)) 0 (PI / 6) _PI2_RLT_0 PI6_RGT_0)... + left; apply PI6_RLT_PI2... - left; apply (Rmult_lt_0_compat (sqrt 3) (/ 2))... + apply Rlt_sqrt3_0... + apply Rinv_0_lt_compat; prove_sup0... - rewrite Rsqr_div'. rewrite cos2; unfold Rsqr; rewrite sin_PI6; rewrite sqrt_def... + field. + left ; prove_sup0. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt