proposition: Lemma apply_big_prod : forall (I : finType) (F : I -> cpoly_cring CR) (x : CR), (\big[cr_mult/One]_i F i) ! x [=] \big[cr_mult/One]_i (F i) ! x.
proof: Proof. move=> I F x. elim:(index_enum I)=>[|j r Hrec] /=. by apply one_apply. rewrite (mult_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