proposition: Lemma NonnegativeRationals_to_Dcuts_corr (q : NonnegativeRationals) : Dcuts_def_corr (λ r : NonnegativeRationals, (r < q)%NRat).
proof: 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.
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