proposition: Lemma monic_bigsum : forall n (I : finType) (F : I -> cpoly_cring CR) (i : I), monic n.+1 (F i) -> (forall j : I, j != i -> degree_le n (F j)) -> monic n.+1 (\big[csg_op/Zero]_i F i).
proof: Proof. move=> n I F i Hmon Hdeg. split; last first. apply bigsum_degree_le=> j. case_eq (i==j). by move/eqP=> <-; apply Hmon. rewrite eq_sym. move/negbT=> Heq. apply (degree_le_mon _ _ n); first by apply le_S; apply le_n. by apply (Hdeg j). rewrite nth_coeff_bigsum. setoid_rewrite (bigD1 (P:=predT) (j:=i) (fun i0 => nth_coeff n.+1 (F i0))); last by done. transitivity ((One : CR)[+]Zero); last by ring. apply csbf_wd; first by apply Hmon. apply big1=> j'. case/andP=> Pj' neqj'. by apply Hdeg. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun paths perm CPoly_Degree Setoid Morphisms Ring CRingClass CPoly_Euclid bigopsClass matrixClass