proposition: Lemma ExpCC_plus : forall z1 z2 : CC, ExpCC (z1[+]z2) [=] ExpCC z1[*]ExpCC z2.
proof: Proof. intros z1 z2. apply eq_transitive_unfolded with (S := cc_csetoid) (y := cc_IR (Exp (Re z1) [*]Exp (Re z2)) [*] ((Cos (Im z1) [*]Cos (Im z2) [-]Sin (Im z1) [*]Sin (Im z2)) [+I*] (Sin (Im z1) [*]Cos (Im z2) [+]Cos (Im z1) [*]Sin (Im z2)))). eapply eq_transitive_unfolded. apply ExpCC_equation_aid_1. apply ExpCC_equation_aid_2. eapply eq_transitive_unfolded. apply ExpCC_equation_aid_3. apply ExpCC_equation_aid_4. Qed.
imports: CoRN.complex.AbsCC CoRN.transc.Exponential CoRN.transc.Pi