Lemma issublinear_invNonnegativeRationals : ∏ x y : NonnegativeRationals, / (x + y) <= / x + / y. Proof. intros x y. generalize (eq0orgt0NonnegativeRationals x) ; apply sumofmaps ; intros Hx0. - rewrite Hx0, islunit_zeroNonnegativeRationals ; clear Hx0 x. now apply plusNonnegativeRationals_le_l. - generalize (eq0orgt0NonnegativeRationals y) ; apply sumofmaps ; intros Hy0. + rewrite Hy0, isrunit_zeroNonnegativeRationals ; clear Hy0 y. now apply plusNonnegativeRationals_le_r. + apply (multNonnegativeRationals_lecompat_l' _ _ _ Hx0). rewrite isldistr_mult_plusNonnegativeRationals, (isrinv_NonnegativeRationals _ Hx0), !(iscomm_multNonnegativeRationals x). apply (multNonnegativeRationals_lecompat_l' _ _ _ Hy0). rewrite isldistr_mult_plusNonnegativeRationals, <- (isassoc_multNonnegativeRationals _ (/ y)%NRat), (isrinv_NonnegativeRationals _ Hy0), islunit_oneNonnegativeRationals, isrunit_oneNonnegativeRationals, (iscomm_multNonnegativeRationals y). apply (multNonnegativeRationals_lecompat_l' (x + y)). * now apply ispositive_plusNonnegativeRationals_l, Hx0. * rewrite <- ! isassoc_multNonnegativeRationals , isrinv_NonnegativeRationals, islunit_oneNonnegativeRationals, isldistr_mult_plusNonnegativeRationals, !isrdistr_mult_plusNonnegativeRationals, !isassoc_plusNonnegativeRationals. ** now apply plusNonnegativeRationals_le_r. ** 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.