proposition: Lemma ExpCC_wd : forall z1 z2 : CC, z1 [=] z2 -> ExpCC z1 [=] ExpCC z2.
proof: Proof. intro z1. elim z1. intros x1 y1. intro z2. elim z2. intros x2 y2. unfold ExpCC in |- *. unfold Re, Im in |- *. intros (H1, H2). simpl in H1. simpl in H2. apply bin_op_wd_unfolded. apply cc_IR_wd. apply Exp_wd. assumption. astepl (Cos y2[+I*]Sin y1). astepl (Cos y2[+I*]Sin y2). apply eq_reflexive. Qed.
imports: CoRN.complex.AbsCC CoRN.transc.Exponential CoRN.transc.Pi