proposition: Lemma nth_coeff_bigops : forall (k : nat) (r : seq nat) F, nth_coeff k (\big[cpoly_plus_cs K/cpoly_zero K]_(i <- r) F i) [=] \big[csg_op/(Zero:K)]_(i <- r) (nth_coeff k (F i)).
proof: Proof. intros. induction r. rewrite big_nil. simpl; reflexivity. rewrite big_cons. rewrite nth_coeff_plus. rewrite IHr. rewrite big_cons. reflexivity. Qed.
imports: ssreflect CSetoids CSetoidFun CFields CPolynomials Program Omega Equivalence Morphisms Wf Morphisms CRings CRing_Homomorphisms Rational Setoid CPoly_NthCoeff CPoly_Degree CReals Intervals CauchySeq IntervalFunct MoreIntervals MoreFunctions Composition seq bigopsClass