proposition: Lemma oddpoly_pos : forall (p : RX) n, Nat.Odd n -> monic n p -> {x : R | [0] [<=] p ! x}.
proof: Proof. intros p n H1 H2. apply cpoly_pos with n; auto. destruct H1 as [m ->]; rewrite Nat.add_1_r; exact (Nat.lt_0_succ _). Qed.
imports: CoRN.reals.IVT