proposition: Lemma NRoot_cancel_less : forall x (Hx:[0][<=]x) y (Hy:[0][<=]y) k (Hk Hk':0<k), NRoot Hx Hk [<] NRoot Hy Hk' -> x [<] y.
proof: Proof. intros x Hx y Hy k Hk Hk' H. astepl (NRoot Hx Hk[^]k). astepr (NRoot Hy Hk'[^]k). apply nexp_resp_less. auto with *. apply NRoot_nonneg. assumption. Qed.
imports: CoRN.reals.OddPolyRootIR