Lemma Dcuts_le_ngt_rel : ∏ x y : Dcuts_set, ¬ Dcuts_lt_rel x y <-> Dcuts_le_rel y x. Proof. intros X Y. split. - intros Hnlt y Yy. generalize (is_Dcuts_open _ _ Yy) ; apply hinhuniv ; intros y'. generalize (pr1 (ispositive_minusNonnegativeRationals _ _) (pr2 (pr2 y'))) ; intros Hy. generalize (is_Dcuts_corr X _ Hy). apply hinhuniv. apply sumofmaps ; [intros nXc | ]. + apply fromempty, Hnlt. apply hinhpr. exists (pr1 y') ; split. * intro Xy' ; apply nXc. apply is_Dcuts_bot with (1 := Xy'). now apply minusNonnegativeRationals_le. * exact (pr1 (pr2 y')). + intros x. apply is_Dcuts_bot with (1 := pr1 (pr2 x)). apply notlt_geNonnegativeRationals ; intro H ; apply Hnlt. apply hinhpr. exists (pr1 x + (pr1 y' - y)) ; split. * exact (pr2 (pr2 x)). * apply is_Dcuts_bot with (1 := pr1 (pr2 y')). pattern (pr1 y') at 2; rewrite <- (minusNonnegativeRationals_plus_r y (pr1 y')). ** rewrite iscomm_plusNonnegativeRationals. apply plusNonnegativeRationals_lecompat_l. now apply lt_leNonnegativeRationals, H. ** apply lt_leNonnegativeRationals ; apply_pr2 ispositive_minusNonnegativeRationals. exact Hy. - intros Hxy ; unfold neg. apply (hinhuniv (P := make_hProp _ isapropempty)) ; intros r. refine (pr1 (pr2 r) _). refine (Hxy _ _). exact (pr2 (pr2 r)). 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.