proposition: Lemma nrCC3_a2 : forall p n, nth_coeff n (Im_poly p) [=] Im (nth_coeff n p).
proof: Proof. intro. elim p; intros. unfold Im_poly in |- *. apply eq_transitive_unfolded with ZeroR. apply eq_reflexive_unfolded. apply eq_transitive_unfolded with (Im ([0]:CC)). apply eq_reflexive_unfolded. apply eq_reflexive_unfolded. elim n; intros. apply eq_transitive_unfolded with (Im s). apply eq_reflexive_unfolded. apply eq_reflexive_unfolded. apply eq_transitive_unfolded with (nth_coeff n0 (Im_poly c)). apply eq_reflexive_unfolded. apply eq_transitive_unfolded with (Im (nth_coeff (R:=CC) n0 c)). apply H. apply eq_reflexive_unfolded. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing