proposition: Lemma degree_le_cpoly_linear : forall (p : cpoly R) c n, degree_le (S n) (c[+X*]p) -> degree_le n p.
proof: Proof. unfold degree_le in |- *. intros. change (nth_coeff (S m) (cpoly_linear _ c p) [=] [0]) in |- *. apply H. auto with arith. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia