proposition: Lemma oddpoly_root : forall f n, Nat.Odd n -> degree n f -> {x : IR | f ! x [=] [0]}.
proof: Proof. intros f n H H0. elim (oddpoly_root' (poly_norm _ f n H0) n); auto. intros. exists x. apply poly_norm_apply with n H0; auto. apply poly_norm_monic; auto. Qed.
imports: CoRN.reals.IVT