proposition: Lemma Cpoly_ex_degree : forall p : RX, {n : nat | degree_le n p}.
proof: Proof. intros. exists (lth_of_poly p). apply poly_degree_lth. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia