proposition: Lemma Sin_plus : forall x y : IR, Sin (x[+]y) [=] Sin x[*]Cos y[+]Cos x[*]Sin y.
proof: Proof. intros. cut (Feq realline (F y) (G y)). intro H. cut (Dom (F y) x). intro H0. cut (Dom (G y) x). intro H1. cut (Part _ _ H0 [=] Part _ _ H1). intro H2. simpl in H2. simpl in |- *. eapply eq_transitive_unfolded. eapply eq_transitive_unfolded. 2: apply H2. algebra. algebra. apply Feq_imp_eq with (fun x : IR => True); auto. repeat split. now exists (I, I). unfold F, G in |- *; apply Sin_plus_fun. Qed.
imports: CoRN.transc.Trigonometric