proposition: Lemma NRoot_str_ext : forall k (Hk Hk':0 < k) x y (Hx:[0][<=]x) (Hy:[0][<=]y), NRoot Hx Hk [#] NRoot Hy Hk' -> x[#]y.
proof: Proof. intros k Hk Hk' x y Hx Hy H0. destruct (ap_imp_less _ _ _ H0) as [H1|H1]. apply less_imp_ap. refine (NRoot_cancel_less _ _ _ _ _ _ _ H1). apply Greater_imp_ap. refine (NRoot_cancel_less _ _ _ _ _ _ _ H1). Qed.
imports: CoRN.reals.OddPolyRootIR