Lemma Dcuts_inv_out : ∏ x, ¬ (X x) -> ∏ y, (x < y)%NRat -> Dcuts_inv_val (/ y)%NRat. Proof. intros x nXx y Hy. apply hinhpr. exists (x / y)%NRat ; repeat split. - intros rx Hrx. unfold divNonnegativeRationals. rewrite iscomm_multNonnegativeRationals. apply multNonnegativeRationals_lecompat_r. apply lt_leNonnegativeRationals, notge_ltNonnegativeRationals. intros H ; apply nXx. now apply X_bot with (1 := Hrx). - apply ispositive_divNonnegativeRationals. + apply notge_ltNonnegativeRationals. intros H ; apply nXx. now apply X_bot with (1 := X_0). + apply istrans_le_lt_ltNonnegativeRationals with (2 := Hy). now apply isnonnegative_NonnegativeRationals. - apply_pr2 (multNonnegativeRationals_ltcompat_r y). + apply istrans_le_lt_ltNonnegativeRationals with (2 := Hy). now apply isnonnegative_NonnegativeRationals. + unfold divNonnegativeRationals. rewrite isassoc_multNonnegativeRationals, islinv_NonnegativeRationals, islunit_oneNonnegativeRationals, isrunit_oneNonnegativeRationals. * exact Hy. * apply istrans_le_lt_ltNonnegativeRationals with (2 := Hy). now apply isnonnegative_NonnegativeRationals. Qed.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals.