proposition: Lemma ExpCC_inv : forall z z_, ([1][/] (ExpCC z) [//]z_) [=] ExpCC [--]z.
proof: Proof. intros z H. astepl (ExpCC z[*]ExpCC [--]z[/] ExpCC z[//]H). rational. Qed.
imports: CoRN.complex.AbsCC CoRN.transc.Exponential CoRN.transc.Pi