proposition: Lemma degree_le_Sum (l: list (cpoly R)) n: (forall p, In p l -> degree_le n p) -> degree_le n (cm_Sum l).
proof: Proof. induction l; intros. apply degree_le_cpoly_zero. change (degree_le n (a [+] cm_Sum l)). apply degree_le_plus; intuition. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia