proposition: Lemma oddpoly_pos' : forall (p : RX) a n, Nat.Odd n -> monic n p -> {x : R | a [<] x | [0] [<=] p ! x}.
proof: Proof. intros p a n H1 H2. elim (Ccpoly_pos' _ p a n). - intros x Hx Hp; exists x; assumption. - destruct H1 as [m ->]; rewrite Nat.add_1_r; exact (Nat.lt_0_succ _). - assumption. Qed.
imports: CoRN.reals.IVT