proposition: Lemma NRoot_pos : forall x Hx k Hk, [0] [<] x -> [0] [<] NRoot x k Hx Hk.
proof: Proof. intros. rename X into H. cut ([0] [<=] NRoot x k Hx Hk); intros. cut (NRoot x k Hx Hk [<] [0] or [0] [<] NRoot x k Hx Hk). intros H1. elim H1; clear H1; intro H1. rewrite -> leEq_def in H0; elim (H0 H1). auto. apply ap_imp_less. apply un_op_strext_unfolded with (nexp_op (R:=IR) k). astepl x; astepr ZeroR. apply pos_ap_zero; auto. apply NRoot_nonneg. Qed.
imports: CoRN.reals.OddPolyRootIR