proposition: Lemma tan_PI3 : tan (PI / 3) = sqrt 3.
proof: Proof. unfold tan; rewrite sin_PI3; rewrite cos_PI3; unfold Rdiv; rewrite Rmult_1_l; rewrite Rinv_inv. rewrite Rmult_assoc; rewrite Rinv_l. - apply Rmult_1_r. - discrR. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt