proposition: Lemma Ccpoly_pos' : forall (p : RX) a n, 0 < n -> monic n p -> {x : R | a [<] x | [0] [<=] p ! x}.
proof: Proof. intros. elim (Ccpoly_big _ _ H H0 [0]). intro x'. intro H1. elim (Cbigger (a[+][1]) x'). intro x. intros. exists x; auto. apply less_leEq_trans with (a[+][1]). apply less_plusOne. auto. Qed.
imports: CoRN.reals.IVT