proposition: Lemma nrCC3_a9 : nth_coeff n nrCC3_poly' [=] a[+I*][--]b.
proof: Proof. unfold nrCC3_poly' in |- *. Hint Resolve nth_coeff_p_mult_c_: algebra. apply eq_transitive_unfolded with (nth_coeff n nrCC3_poly''[*] (a[+I*][--]b)). apply nth_coeff_p_mult_c_. Hint Resolve nrCC3_a6: algebra. apply eq_transitive_unfolded with ([1][*] (a[+I*][--]b)). apply bin_op_wd_unfolded. exact nrCC3_a6. apply eq_reflexive_unfolded. apply one_mult. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing