proposition: Lemma degree_le_mult_constant_l (p: cpoly R) (x: R) (n: nat): degree_le n p -> degree_le n (_C_ x [*] p).
proof: Proof. Proof with auto. intros. replace n with (0 + n)%nat... apply degree_le_mult... apply degree_le_c_. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia