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