proposition: Lemma oddpoly_root' : forall f n, Nat.Odd n -> monic n f -> {x : IR | f ! x [=] [0]}.
proof: Proof. intros. elim (oddpoly_neg _ f n); auto. intro a. intro H1. elim (oddpoly_pos' _ f a n); auto. intro b. intros H2 H3. cut {x : IR | a [<=] x /\ x [<=] b /\ f ! x [=] [0]}. intro H4. elim H4. clear H4. intros x H4. elim H4. clear H4. intros H4 H5. elim H5. clear H5. intros. exists x. auto. apply Civt_poly; auto. apply monic_apzero with n; auto. Qed.
imports: CoRN.reals.IVT