proposition: Lemma tan_0 : tan 0 = 0.
proof: Proof. unfold tan in |- *; rewrite sin_0; rewrite cos_0. unfold Rdiv in |- *; apply Rmult_0_l. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Rtrigo_def Rtrigo_alt Cos_rel Cos_plus ZArith_base Zcomplements Lia Lra Ranalysis1 Rsqrt_def PSeries_reg