proposition: Lemma ExpCC_equation_aid_1 : forall z1 z2 : CC, ExpCC (z1[+]z2) [=] cc_IR (Exp (Re z1[+]Re z2)) [*] (Cos (Im z1[+]Im z2) [+I*]Sin (Im z1[+]Im z2)).
proof: Proof. intro z1. elim z1. intros x1 y1. intro z2. elim z2. intros x2 y2. unfold Re, Im in |- *. unfold ExpCC in |- *. apply bin_op_wd_unfolded. apply cc_IR_wd. apply Exp_wd. algebra. split; algebra. Qed.
imports: CoRN.complex.AbsCC CoRN.transc.Exponential CoRN.transc.Pi