proposition: Lemma degree_le_Product (l: list (cpoly R)) n: (forall p, In p l -> degree_le n p) -> degree_le (length l * n) (cr_Product l).
proof: Proof. induction l; intros. apply (degree_le_c_ [1]). change (degree_le (n + length l * n) (a [*] cr_Product l)). apply degree_le_mult; intuition. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia