proposition: Lemma apply_bigops : forall (r : seq K) F x, (\big[cpoly_mult_cs K/cpoly_one K]_(i <- r) F i) ! x [=] \big[cr_mult/(One:K)]_(i <- r) ((F i) ! x).
proof: Proof. intros r F x; destruct r; simpl. rewrite cring_mult_zero; algebra. induction r. simpl; rewrite mult_one; rewrite cpoly_mult_one. reflexivity. repeat rewrite big_cons; simpl in IHr; rewrite mult_assoc. rewrite (mult_commutes K (cpoly_apply K (F s) x) (cpoly_apply K (F t) x)). rewrite <- mult_assoc; rewrite <- IHr. set (@mult_apply); simpl in s0; rewrite <- s0. rewrite cpoly_mult_fast_equiv. set (@cpoly_mult_assoc); unfold CSetoids.associative in a. simpl in a; repeat rewrite a. rewrite (cpoly_mult_commutative K (F s) (F t)). 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