proposition: Lemma tan_plus : 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 tan in |- *; rewrite sin_plus; rewrite cos_plus; unfold Rdiv in |- *; replace (cos x * cos y - sin x * sin y) with (cos x * cos y * (1 - sin x * / cos x * (sin y * / cos y))). - rewrite Rinv_mult. repeat rewrite <- Rmult_assoc; replace ((sin x * cos y + cos x * sin y) * / (cos x * cos y)) with (sin x * / cos x + sin y * / cos y). + reflexivity. + rewrite Rmult_plus_distr_r; rewrite Rinv_mult. repeat rewrite Rmult_assoc; repeat rewrite (Rmult_comm (sin x)); repeat rewrite <- Rmult_assoc. repeat rewrite Rmult_inv_r_id_m; [ reflexivity | assumption | assumption ]. - unfold Rminus in |- *; rewrite Rmult_plus_distr_l; rewrite Rmult_1_r; apply Rplus_eq_compat_l; repeat rewrite Rmult_assoc; rewrite (Rmult_comm (sin x)); rewrite (Rmult_comm (cos y)); rewrite <- Ropp_mult_distr_r_reverse; repeat rewrite <- Rmult_assoc; rewrite Rinv_r. + rewrite Rmult_1_l; rewrite (Rmult_comm (sin x)); rewrite <- Ropp_mult_distr_r_reverse; repeat rewrite Rmult_assoc; apply Rmult_eq_compat_l; rewrite (Rmult_comm (/ cos y)); rewrite Rmult_assoc; rewrite Rinv_r. * apply Rmult_1_r. * assumption. + 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