Lemma ispositive_minusNonnegativeRationals : ∏ x y : NonnegativeRationals, (x < y) <-> (0 < y - x). Proof. intros x y. split ; intro Hlt. - apply_pr2 (plusNonnegativeRationals_ltcompat_r x). rewrite islunit_zeroNonnegativeRationals, minusNonnegativeRationals_plus_r. + exact Hlt. + now apply lt_leNonnegativeRationals, Hlt. - revert Hlt. unfold minusNonnegativeRationals, hnnq_minus. generalize (hqgthorleh (pr1 y) (pr1 x)). apply (coprod_rect (λ _, _ → _)) ; intros H0 ; intro Hlt. + exact H0. + now apply isirrefl_ltNonnegativeRationals in 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.