proposition: Lemma tan_neg : forall x:R, tan (- x) = - tan x.
proof: Proof. intros x; unfold tan in |- *; rewrite sin_neg; rewrite cos_neg; unfold Rdiv in |- *. apply Ropp_mult_distr_l_reverse. 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