proposition: Lemma NRoot_less_one : forall x Hx k Hk, x [<] [1] -> NRoot x k Hx Hk [<] [1].
proof: Proof. intros. apply power_cancel_less with k. apply less_leEq; apply pos_one. eapply less_wdl. 2: apply eq_symmetric_unfolded; apply NRoot_power. astepr OneR. assumption. Qed.
imports: CoRN.reals.OddPolyRootIR