proposition: Lemma degree_le_cpoly_linear_inv (p: cpoly R) (c: R) (n: nat): degree_le n p -> degree_le (S n) (c[+X*]p).
proof: Proof. intros H [|m] E. inversion E. apply (H m). auto with arith. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia