proposition: Lemma tan_diff : forall x y:R, cos x <> 0 -> cos y <> 0 -> tan x - tan y = sin (x - y) / (cos x * cos y).
proof: Proof. intros; unfold tan in |- *; rewrite sin_minus. field. now split. 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