proposition: Lemma NRoot_unique : forall k Hk, [0] [<] x -> x[^]k [=] y -> x [=] NRoot y k Hy Hk.
proof: Proof. intros. rename H into H0. apply root_unique with k; auto. apply NRoot_nonneg. eapply eq_transitive_unfolded. apply H0. apply eq_symmetric_unfolded; apply NRoot_power. Qed.
imports: CoRN.reals.OddPolyRootIR