Lemma iscotrans_Dcuts_lt_rel : iscotrans Dcuts_lt_rel. Proof. intros x y z. apply hinhuniv ; intros r. generalize (is_Dcuts_open _ _ (pr2 (pr2 r))) ; apply hinhuniv ; intros r'. assert (Hr0 : 0%NRat < pr1 r' - pr1 r). { apply ispositive_minusNonnegativeRationals. exact (pr2 (pr2 r')). } generalize (is_Dcuts_corr y _ Hr0) ; apply hinhuniv ; apply sumofmaps ; [intros Yq | intros q]. - apply squash_element ; right ; apply squash_element. exists (pr1 r') ; split. + intro H0 ; apply Yq. apply is_Dcuts_bot with (pr1 r'). * exact H0. * now apply minusNonnegativeRationals_le. + exact (pr1 (pr2 r')). - generalize (isdecrel_leNonnegativeRationals (pr1 q + (pr1 r' - pr1 r)) (pr1 r')) ; apply sumofmaps ; intros Hdec. + apply hinhpr ; right ; apply hinhpr. exists (pr1 r') ; split. * intro Yr' ; apply (pr2 (pr2 q)). apply is_Dcuts_bot with (pr1 r'). ** exact Yr'. ** exact Hdec. * exact (pr1 (pr2 r')). + apply hinhpr ; left ; apply hinhpr. exists (pr1 q) ; split. * intro Xq ; apply (pr1 (pr2 r)). apply is_Dcuts_bot with (pr1 q). ** exact Xq. ** apply notge_ltNonnegativeRationals in Hdec. apply (plusNonnegativeRationals_ltcompat_r (pr1 r)) in Hdec ; rewrite isassoc_plusNonnegativeRationals, minusNonnegativeRationals_plus_r, iscomm_plusNonnegativeRationals in Hdec. *** apply_pr2_in plusNonnegativeRationals_ltcompat_r Hdec. now apply lt_leNonnegativeRationals, Hdec. *** now apply lt_leNonnegativeRationals, (pr2 (pr2 r')). * exact (pr1 (pr2 q)). 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.