proposition: Theorem cos_plus : forall x y:R, cos (x + y) = cos x * cos y - sin x * sin y.
proof: Proof. intros. cut (Un_cv (C1 x y) (cos x * cos y - sin x * sin y)). { assert (Un_cv (C1 x y) (cos (x + y))) by apply C1_cvg. intros. apply UL_sequence with (C1 x y); assumption. } unfold Un_cv; unfold Rdist. intros. assert (H0 := A1_cvg x). assert (H1 := A1_cvg y). assert (H2 := B1_cvg x). assert (H3 := B1_cvg y). assert (H4 := CV_mult _ _ _ _ H0 H1). assert (H5 := CV_mult _ _ _ _ H2 H3). assert (H6 := reste_cv_R0 x y). unfold Un_cv in H4; unfold Un_cv in H5; unfold Un_cv in H6. unfold Rdist in H4; unfold Rdist in H5; unfold Rdist in H6. cut (0 < eps / 3); [ intro | unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. elim (H4 (eps / 3) H7); intros N1 H8. elim (H5 (eps / 3) H7); intros N2 H9. elim (H6 (eps / 3) H7); intros N3 H10. set (N := S (S (max (max N1 N2) N3))). exists N. intros. assert (n = S (pred n)) by lia. rewrite H12. rewrite <- cos_plus_form. 2:lia. rewrite <- H12. apply Rle_lt_trans with (Rabs (A1 x n * A1 y n - cos x * cos y) + Rabs (sin x * sin y - B1 x (pred n) * B1 y (pred n) + Reste x y (pred n))). { replace (A1 x n * A1 y n - B1 x (pred n) * B1 y (pred n) + Reste x y (pred n) - (cos x * cos y - sin x * sin y)) with (A1 x n * A1 y n - cos x * cos y + (sin x * sin y - B1 x (pred n) * B1 y (pred n) + Reste x y (pred n))); [ apply Rabs_triang | ring ]. } replace eps with (eps / 3 + (eps / 3 + eps / 3)) by field. apply Rplus_lt_compat. { apply H8. lia. } apply Rle_lt_trans with (Rabs (sin x * sin y - B1 x (pred n) * B1 y (pred n)) + Rabs (Reste x y (pred n))). { apply Rabs_triang. } apply Rplus_lt_compat. { rewrite <- Rabs_Ropp. rewrite Ropp_minus_distr. apply H9. lia. } replace (Reste x y (pred n)) with (Reste x y (pred n) - 0) by ring. apply H10. lia. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_def Cos_rel Lia Lra