proposition: Lemma monic_bigprod : forall (I : finType) (F : I -> cpoly_cring CR) (deg : I -> nat), (forall i : I, monic (deg i) (F i)) -> monic (\big[addn/0]_i deg i) (\big[cr_mult/One]_i F i).
proof: Proof. move=> I F deg Hdeg. elim:(index_enum I)=>[|i r Hrec]. by apply monic_c_one. simpl. by apply monic_mult. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun paths perm CPoly_Degree Setoid Morphisms Ring CRingClass CPoly_Euclid bigopsClass matrixClass