proposition: Lemma ExpCC_Periodic : forall z, ExpCC (z[+]II[*]Two[*]cc_IR Pi) [=] ExpCC z.
proof: Proof. intro z. elim z. intros x y. astepl (ExpCC (x[+I*] (y[+]Two[*]Pi))). unfold ExpCC in |- *. apply bin_op_wd_unfolded. apply cc_IR_wd. apply Exp_wd. simpl in |- *. apply eq_reflexive_unfolded. astepl (Cos (y[+]Two[*]Pi) [+I*]Sin (y[+]Two[*]Pi)). astepl (Cos y[+I*]Sin y). apply eq_reflexive. apply ExpCC_wd. split; simpl in |- *; rational. Qed.
imports: CoRN.complex.AbsCC CoRN.transc.Exponential CoRN.transc.Pi