proposition: Lemma issublinear_invNonnegativeRationals_lt : ∏ x y : NonnegativeRationals, (0 < x)%NRat -> (0 < y)%NRat -> (/ (x + y) < / x + / y)%NRat.
proof: 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.
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