proposition: Theorem Euler : (ExpCC (II[*] (cc_IR Pi))) [+][1] [=] [0].
proof: Proof. split. Opaque Sin Cos Exp. simpl. rstepl ((Exp [0]) [*] (Cos Pi) [+][1]). astepl (([1]:IR) [*][--][1][+][1]). rational. simpl. rstepl ((Exp [0]) [*] (Sin Pi)). Step_final (([1]:IR) [*][0]). Qed.
imports: CoRN.complex.AbsCC CoRN.transc.Exponential CoRN.transc.Pi