proposition: Lemma noteq_ltorgtNonnegativeRationals : ∏ x y : NonnegativeRationals, x != y -> (x < y) ⨿ (x > y).
proof: 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.
imports: UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.RealNumbers.Sets UniMath.RealNumbers.Fields UniMath.Algebra.DivisionRig UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim