proposition: Lemma NRoot_wd : forall k Hk Hk', x [=] y -> NRoot x k Hx Hk [=] NRoot y k Hy Hk'.
proof: Proof. intros. apply root_unique with k; auto. apply NRoot_nonneg. apply NRoot_nonneg. eapply eq_transitive_unfolded. eapply eq_transitive_unfolded. 2: apply H. apply NRoot_power. apply eq_symmetric_unfolded; apply NRoot_power. Qed.
imports: CoRN.reals.OddPolyRootIR