proposition: Lemma tan_minus : forall x y:R, cos x <> 0 -> cos y <> 0 -> cos (x - y) <> 0 -> 1 + tan x * tan y <> 0 -> tan (x - y) = (tan x - tan y) / (1 + tan x * tan y).
proof: Proof. intros; unfold Rminus in |- *; rewrite tan_plus. - rewrite tan_neg; unfold Rminus in |- *; rewrite <- Ropp_mult_distr_l_reverse; rewrite Rmult_opp_opp; reflexivity. - assumption. - rewrite cos_neg; assumption. - assumption. - rewrite tan_neg; unfold Rminus in |- *; rewrite <- Ropp_mult_distr_l_reverse; rewrite Rmult_opp_opp; 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