Lemma noteq_ltorgtNonnegativeRationals : ∏ x y : NonnegativeRationals, x != y -> (x < y) ⨿ (x > y). Proof. intros x y Hneq. generalize (isdecrel_leNonnegativeRationals x y) ; apply sumofmaps ; [intros Hle|intros Hlt]. - left. apply le_eqorltNonnegativeRationals in Hle. revert Hle ; apply sumofmaps ; [intros Heq | intros Hlt]. + now apply fromempty, Hneq, Heq. + exact Hlt. - right. apply neghqgehtolth. exact Hlt. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.RealNumbers.Fields. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim.