Lemma isapfun_NonnegativeRationals_to_Dcuts_aux : ∏ q q' : NonnegativeRationals, NonnegativeRationals_to_Dcuts q < NonnegativeRationals_to_Dcuts q' <-> (q < q')%NRat. Proof. intros q q'. split. - apply hinhuniv. intros r. apply istrans_le_lt_ltNonnegativeRationals with (pr1 r). + apply notlt_geNonnegativeRationals. exact (pr1 (pr2 r)). + exact (pr2 (pr2 r)). - intros H. apply hinhpr. exists q ; split. + now apply (isirrefl_ltNonnegativeRationals q). + exact H. 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.