proposition: Lemma degree_le_zero : forall p : RX, degree_le 0 p -> {a : R | p [=] _C_ a}.
proof: Proof. unfold degree_le in |- *. intros. exists (nth_coeff 0 p). apply all_nth_coeff_eq_imp. intros. elim (O_or_S i); intro y. elim y. clear y. intros x y. rewrite <- y. cut (0 < S x). intro. Step_final ([0]:R). auto with arith. rewrite <- y. algebra. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia