proposition: Lemma ExpCC_equation_aid_2 : forall z1 z2 : CC, cc_IR (Exp (Re z1[+]Re z2)) [*] (Cos (Im z1[+]Im z2) [+I*]Sin (Im z1[+]Im z2)) [=] 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))).
proof: Proof. intros z1 z2. apply bin_op_wd_unfolded. apply cc_IR_wd. algebra. split; algebra. Qed.
imports: CoRN.complex.AbsCC CoRN.transc.Exponential CoRN.transc.Pi