proposition: Lemma tan_PI6 : tan (PI / 6) = 1 / sqrt 3.
proof: Proof. unfold tan; rewrite sin_PI6; rewrite cos_PI6; unfold Rdiv; repeat rewrite Rmult_1_l; rewrite Rinv_mult. rewrite Rinv_inv. rewrite (Rmult_comm (/ 2)); rewrite Rmult_assoc; rewrite Rinv_r. - apply Rmult_1_r. - discrR. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt