proposition: Lemma isapfun_NonnegativeRationals_to_Dcuts_aux : ∏ q q' : NonnegativeRationals, NonnegativeRationals_to_Dcuts q < NonnegativeRationals_to_Dcuts q' <-> (q < q')%NRat.
proof: 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.
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