proposition: Lemma ispositive_minusNonnegativeRationals : ∏ x y : NonnegativeRationals, (x < y) <-> (0 < y - x).
proof: 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.
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