proposition: Lemma nth_coeff_bigsum : forall n (I : finType) (F : I -> cpoly_cring CR), nth_coeff n (\big[csg_op/Zero]_i (F i)) [=] \big[csg_op/Zero]_i (nth_coeff n (F i)).
proof: Proof. move=> n I F. have Hz : nth_coeff n Zero [=] (Zero : CR) by reflexivity. have Hplus : forall p q : cpoly_cring CR, nth_coeff n (p[+]q) [=] nth_coeff n p [+] nth_coeff n q. by move=> p q; apply nth_coeff_plus. by apply (big_morph Hplus Hz _ predT). Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun paths perm CPoly_Degree Setoid Morphisms Ring CRingClass CPoly_Euclid bigopsClass matrixClass