Lemma ispositive_Dcuts_minus : ∏ x y : Dcuts, (y < x) <-> (0 < Dcuts_minus x y). Proof. intros X Y. split. - apply hinhuniv ; intros x. generalize (is_Dcuts_open _ _ (pr2 (pr2 x))) ; apply hinhfun ; intros x'. exists 0%NRat ; split. + now apply (isnonnegative_NonnegativeRationals' 0%NRat). + apply hinhpr. exists (pr1 x') ; split. * exact (pr1 (pr2 x')). * intros y ; apply sumofmaps ; [intros Yy | intros ->]. ** rewrite islunit_zeroNonnegativeRationals. apply istrans_ltNonnegativeRationals with (pr1 x). *** apply (Dcuts_finite Y). { exact (pr1 (pr2 x)). } exact Yy. *** exact (pr2 (pr2 x')). ** rewrite islunit_zeroNonnegativeRationals. apply istrans_le_lt_ltNonnegativeRationals with (pr1 x). *** now apply isnonnegative_NonnegativeRationals. *** exact (pr2 (pr2 x')). - apply hinhuniv ; intros r ; generalize (pr2 (pr2 r)). apply hinhfun ; intros x. exists (pr1 x) ; split. + intros Yx ; apply (isnonnegative_NonnegativeRationals' (pr1 r)). apply_pr2 (plusNonnegativeRationals_ltcompat_r (pr1 x)). rewrite islunit_zeroNonnegativeRationals. now apply (pr2 (pr2 x)) ; left. + exact (pr1 (pr2 x)). 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.