Lemma divNonnegativeRationals_le1 : ∏ q r : NonnegativeRationals, q <= r -> q / r <= 1. Proof. intros q r Hrq. generalize (eq0orgt0NonnegativeRationals r) ; apply sumofmaps ; intros Hr0. - unfold divNonnegativeRationals. rewrite Hr0, inv_zeroNonnegativeRationals. rewrite israbsorb_zero_multNonnegativeRationals. now apply isnonnegative_NonnegativeRationals. - apply (multNonnegativeRationals_lecompat_r' r). + exact Hr0. + unfold divNonnegativeRationals. rewrite isassoc_multNonnegativeRationals, islinv_NonnegativeRationals. * rewrite isrunit_oneNonnegativeRationals, islunit_oneNonnegativeRationals. exact Hrq. * exact Hr0. 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.