proposition: Lemma oddpoly_neg : forall (p : RX) n, Nat.Odd n -> monic n p -> {x : R | p ! x [<=] [0]}.
proof: Proof. intros. elim (oddpoly_pos _ _ H (flip_odd _ _ _ H H0)). intro x. intros. exists ( [--]x). astepl ( [--][--]p ! ( [--]x)). astepr ( [--] ([0]:R)). apply inv_resp_leEq. astepr (flip _ p) ! x. auto. Qed.
imports: CoRN.reals.IVT