proposition: Lemma issublinear_invNonnegativeRationals : ∏ x y : NonnegativeRationals, / (x + y) <= / x + / y.
proof: 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.
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