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