proposition: Lemma Dcuts_inv_out : ∏ x, ¬ (X x) -> ∏ y, (x < y)%NRat -> Dcuts_inv_val (/ y)%NRat.
proof: 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.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations UniMath.RealNumbers.Sets UniMath.Algebra.ConstructiveStructures UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim UniMath.RealNumbers.NonnegativeRationals