proposition: Lemma ExpCC_Exp : forall x : IR, ExpCC (cc_IR x) [=] cc_IR (Exp x).
proof: Proof. intro x. unfold ExpCC in |- *. astepl (cc_IR (Exp x) [*] (Cos (Im (cc_IR x)) [+I*]Sin (Im (cc_IR x)))). astepr (cc_IR (Exp x) [*][1]). apply bin_op_wd_unfolded. algebra. astepl (Cos [0][+I*]Sin [0]). Step_final ([1][+I*][0]). Qed.
imports: CoRN.complex.AbsCC CoRN.transc.Exponential CoRN.transc.Pi