proposition: Lemma ExpCC_inv_aid : forall z : CC, ExpCC z[*]ExpCC [--]z [=] [1].
proof: Proof. intro z. apply eq_transitive_unfolded with (S := cc_csetoid) (y := ExpCC [0]). astepl (ExpCC (z[+][--]z)). apply ExpCC_wd. rational. algebra. Qed.
imports: CoRN.complex.AbsCC CoRN.transc.Exponential CoRN.transc.Pi