proposition: Lemma ExpCC_Zero : ExpCC [0] [=] [1].
proof: Proof. unfold ExpCC in |- *. astepl (cc_IR (Exp [0]) [*] (Cos [0][+I*]Sin [0])). astepl (cc_IR [1][*] (Cos [0][+I*]Sin [0])). astepl (cc_IR [1][*] ([1][+I*][0])). simpl in |- *. split; simpl in |- *; rational. Qed.
imports: CoRN.complex.AbsCC CoRN.transc.Exponential CoRN.transc.Pi