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