proposition: Lemma Cos_plus : forall x y : IR, Cos (x[+]y) [=] Cos x[*]Cos y[-]Sin x[*]Sin y.
proof: Proof. intros. elim (Cos_plus_fun y). intros. elim b; intros H H0. cut (Dom (Cosine[o]FId{+}[-C-]y) x). intro H1. cut (Dom (Cosine{*}[-C-] (Cos y) {-}Sine{*}[-C-] (Sin y)) x). intro H2. simpl in H0. simpl in |- *. eapply eq_transitive_unfolded. eapply eq_transitive_unfolded. 2: apply (H0 x I H1 H2). algebra. algebra. repeat split. now exists (I, I). Qed.
imports: CoRN.transc.Trigonometric