proposition: Lemma NRoot_resp_leEq : forall x y xpos ypos k kpos, x [<=] y -> NRoot (x:=x) (n:=k) xpos kpos [<=] NRoot (x:=y) (n:=k) ypos kpos.
proof: Proof. intros. rewrite -> leEq_def; intro H0. assert (NRoot ypos kpos[^]k [<=] NRoot xpos kpos[^]k). apply power_resp_leEq. apply NRoot_nonneg. apply less_leEq; auto. assert (x [=] y). apply leEq_imp_eq; auto. eapply leEq_wdl. eapply leEq_wdr. eexact H1. algebra. algebra. clear H H1. generalize (NRoot_wd _ _ xpos ypos k kpos kpos H2). intro. apply (less_irreflexive_unfolded _ (NRoot ypos kpos)). astepr (NRoot xpos kpos). auto. Qed.
imports: CoRN.reals.OddPolyRootIR