proposition: Lemma degree_imp_degree_le : forall (p : RX) n, degree n p -> degree_le n p.
proof: Proof. unfold degree in |- *. intros p n H. elim H. auto. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia