proposition: Lemma apply_bigsum : forall (I : finType) (F : I -> cpoly_cring CR) (x : CR), (\big[csg_op/Zero]_i F i) ! x [=] \big[csg_op/Zero]_i (F i) ! x.
proof: Proof. move=> I F x. elim:(index_enum I)=>[|j r Hrec] /=. by apply poly_eq_zero; reflexivity. rewrite (plus_apply _ (F j)). by rewrite Hrec; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun paths perm CPoly_Degree Setoid Morphisms Ring CRingClass CPoly_Euclid bigopsClass matrixClass