proposition: Lemma NRoot_pres_less : forall x Hx y Hy k Hk, x [<] y -> NRoot x k Hx Hk [<] NRoot y k Hy Hk.
proof: Proof. intros. apply power_cancel_less with k. apply NRoot_nonneg. eapply less_wdl. 2: apply eq_symmetric_unfolded; apply NRoot_power. eapply less_wdr. 2: apply eq_symmetric_unfolded; apply NRoot_power. auto. Qed.
imports: CoRN.reals.OddPolyRootIR