proposition: Lemma ExpCC_ap_zero : forall z : CC, ExpCC z [#] [0].
proof: Proof. intro z. cut (ExpCC z[*]ExpCC [--]z [#] [0]). intro H. apply (mult_cancel_ap_zero_lft _ _ _ H). astepl ([1]:CC). apply cc_cr_non_triv. Qed.
imports: CoRN.complex.AbsCC CoRN.transc.Exponential CoRN.transc.Pi