proposition: Lemma realpolyn_oddhaszero : forall f, odd_cpoly _ f -> {x : IR | f ! x [=] [0]}.
proof: Proof. unfold odd_cpoly in |- *. intros f H. elim H. clear H. intro n. intros H H0. cut (Nat.Odd n). intro. elim (oddpoly_root f n H1 H0). intros. exists x. auto. apply Codd_to. assumption. Qed.
imports: CoRN.reals.IVT