Lemma issublinear_invNonnegativeRationals_lt : ∏ x y : NonnegativeRationals, (0 < x)%NRat -> (0 < y)%NRat -> (/ (x + y) < / x + / y)%NRat. Proof. intros x y Hx0 Hy0. apply_pr2 (multNonnegativeRationals_ltcompat_l x). - exact Hx0. - rewrite isldistr_mult_plusNonnegativeRationals, (isrinv_NonnegativeRationals _ Hx0), !(iscomm_multNonnegativeRationals x). apply_pr2 (multNonnegativeRationals_ltcompat_l y). + exact Hy0. + rewrite isldistr_mult_plusNonnegativeRationals, <- (isassoc_multNonnegativeRationals _ (/ y)%NRat), (isrinv_NonnegativeRationals _ Hy0), islunit_oneNonnegativeRationals, isrunit_oneNonnegativeRationals, (iscomm_multNonnegativeRationals y). apply_pr2 (multNonnegativeRationals_ltcompat_l (x + y)). * apply ispositive_plusNonnegativeRationals_l. exact Hx0. * rewrite <- ! isassoc_multNonnegativeRationals , isrinv_NonnegativeRationals, islunit_oneNonnegativeRationals, isldistr_mult_plusNonnegativeRationals, !isrdistr_mult_plusNonnegativeRationals, !isassoc_plusNonnegativeRationals. ** apply plusNonnegativeRationals_lt_r. apply ispositive_plusNonnegativeRationals_l. now apply ispositive_multNonnegativeRationals ; apply Hy0. ** now apply ispositive_plusNonnegativeRationals_l, Hx0. 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.