proposition: Lemma nrCC3_a7 : forall r : IR, nrCC3_poly' ! (cc_IR r) [=] (r[+I*][1]) [^]n[*] (a[+I*][--]b).
proof: Proof. intros. unfold nrCC3_poly' in |- *. apply eq_transitive_unfolded with (nrCC3_poly'' ! (cc_IR r) [*] (_C_ (a[+I*][--]b)) ! (cc_IR r)). apply mult_apply. Hint Resolve nrCC3_a3: algebra. apply eq_transitive_unfolded with (nrCC3_poly'' ! (cc_IR r) [*] (a[+I*][--]b)). apply bin_op_wd_unfolded. apply eq_reflexive_unfolded. apply c_apply. apply bin_op_wd_unfolded. apply nrCC3_a3. apply eq_reflexive_unfolded. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing