Lemma Dcuts_minus_plus_max : ∏ x y : Dcuts, Dcuts_plus (Dcuts_minus x y) y = Dcuts_max x y. Proof. intros X Y. apply Dcuts_eq_is_eq ; intros r ; split. - apply hinhuniv ; apply sumofmaps ; [ apply sumofmaps ; [intros XYr | intros Yr] | intros xyy ; rewrite (pr1 (pr2 xyy))]. + apply hinhpr ; left. revert XYr ; now refine (Dcuts_minus_le _ _ _). + now apply hinhpr ; right. + generalize (pr1 (pr2 (pr2 xyy))) ; apply hinhfun ; intros x. left ; apply is_Dcuts_bot with (1 := pr1 (pr2 x)). apply lt_leNonnegativeRationals. apply (pr2 (pr2 x)). left. exact (pr2 (pr2 (pr2 xyy))). - apply hinhuniv ; apply sumofmaps ; [intros Xr|intros Yr]. + generalize (is_Dcuts_open _ _ Xr) ; apply hinhuniv ; intros x. generalize (pr1 (ispositive_minusNonnegativeRationals _ _) (pr2 (pr2 x))) ; intros Hx. generalize (is_Dcuts_corr Y _ Hx) ; apply hinhuniv ; apply sumofmaps ; [ intros nYx | intros Hyx ] ; apply_pr2_in ispositive_minusNonnegativeRationals Hx. * rewrite <- (Dcuts_minus_plus_r (Dcuts_minus X Y) X Y). ** exact Xr. ** apply Dcuts_lt_le_rel. apply hinhpr ; exists (pr1 x - r) ; split. { exact nYx. } apply is_Dcuts_bot with (1 := pr1 (pr2 x)). now apply minusNonnegativeRationals_le. ** reflexivity. * rename Hyx into y. generalize (pr2 (pr2 y)) ; intros nYy. rewrite iscomm_plusNonnegativeRationals, minusNonnegativeRationals_plus_exchange in nYy. 2: now apply lt_leNonnegativeRationals. generalize (isdecrel_leNonnegativeRationals r (pr1 y)) ; apply sumofmaps ; intros Hle. { apply hinhpr ; left ; right. now apply is_Dcuts_bot with (1 := pr1 (pr2 y)). } apply notge_ltNonnegativeRationals in Hle. rewrite <- (Dcuts_minus_plus_r (Dcuts_minus X Y) X Y). ** exact Xr. ** apply Dcuts_lt_le_rel. apply hinhpr ; exists ((pr1 x + pr1 y) - r) ; split. { exact nYy. } apply is_Dcuts_bot with (1 := pr1 (pr2 x)). pattern (pr1 x) at 2; rewrite <- (plusNonnegativeRationals_minus_r r (pr1 x)). apply minusNonnegativeRationals_lecompat_l. apply plusNonnegativeRationals_lecompat_l. now apply lt_leNonnegativeRationals. ** reflexivity. + now apply hinhpr ; left ; right. 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.