proposition: Lemma bigprod_degree_le : forall (I : finType) (P : pred I) (F : I -> cpoly_cring CR) (deg : I -> nat), (forall i : I, P i -> degree_le (deg i) (F i)) -> degree_le (\big[addn/0]_(i|P i) (deg i)) (\big[cr_mult/One]_(i|P i) (F i)).
proof: Proof. move=> I P F deg Hdeg. generalize (index_enum I). elim=>[|i r Hrec]. case; [case/lt_irrefl|reflexivity]. simpl; have{Hdeg}:=Hdeg i. case: (P i)=> Hi; last by apply Hrec. by apply degree_le_mult; [apply Hi|apply Hrec]. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun paths perm CPoly_Degree Setoid Morphisms Ring CRingClass CPoly_Euclid bigopsClass matrixClass