proposition: Lemma nrCC3_a3 : forall r : IR, nrCC3_poly'' ! (cc_IR r) [=] (r[+I*][1]) [^]n.
proof: Proof. intros. unfold nrCC3_poly'' in |- *. apply eq_transitive_unfolded with ((_X_[+]_C_ II) ! (cc_IR r) [^]n). apply nexp_apply. apply eq_transitive_unfolded with ((_X_ ! (cc_IR r) [+] (_C_ II) ! (cc_IR r)) [^]n). apply un_op_wd_unfolded. apply plus_apply. cut (forall c x : CC, _X_ ! x[+] (_C_ c) ! x [=] x[+]c); intros. apply eq_transitive_unfolded with ((cc_IR r[+]II) [^]n). apply un_op_wd_unfolded. apply H. apply eq_transitive_unfolded with ((r[+I*][0][+][0][+I*][1]) [^]n). apply eq_reflexive_unfolded. apply eq_transitive_unfolded with (((r[+][0]) [+I*] ([0][+][1])) [^]n). apply eq_reflexive_unfolded. apply un_op_wd_unfolded. apply I_wd. apply cm_rht_unit_unfolded. apply cm_lft_unit_unfolded. apply bin_op_wd_unfolded. apply x_apply. apply c_apply. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing