proposition: Lemma divNonnegativeRationals_le1 : ∏ q r : NonnegativeRationals, q <= r -> q / r <= 1.
proof: 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.
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