proposition: Lemma tan_2a : forall x:R, cos x <> 0 -> cos (2 * x) <> 0 -> 1 - tan x * tan x <> 0 -> tan (2 * x) = 2 * tan x / (1 - tan x * tan x).
proof: Proof. repeat rewrite <-Rplus_diag; intros; repeat rewrite <-Rplus_diag; rewrite <-Rplus_diag in H0; apply tan_plus; assumption. 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