Lemma NonnegativeRationals_to_Dcuts_corr (q : NonnegativeRationals) : Dcuts_def_corr (λ r : NonnegativeRationals, (r < q)%NRat). Proof. intros r Hr0. apply hinhpr. generalize (isdecrel_ltNonnegativeRationals r q) ; apply sumofmaps ; intros Hqr. - right. assert (Hn0 : (0 < q - r)%NRat) by (now apply ispositive_minusNonnegativeRationals). exists (q - r). split. + apply_pr2 (plusNonnegativeRationals_ltcompat_r r). rewrite minusNonnegativeRationals_plus_r. * pattern q at 1 ; rewrite <- isrunit_zeroNonnegativeRationals. apply plusNonnegativeRationals_ltcompat_l. exact Hr0. * now apply lt_leNonnegativeRationals, Hqr. + rewrite minusNonnegativeRationals_plus_r. * now apply isirrefl_ltNonnegativeRationals. * now apply lt_leNonnegativeRationals, Hqr. - now left. 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.