Lemma Dcuts_minus_plus_r: ∏ x y z : Dcuts, z <= y -> x = Dcuts_minus y z -> y = Dcuts_plus x z. Proof. intros _ Y Z Hyz ->. apply Dcuts_eq_is_eq ; intro r ; split. - intros Yr. generalize (is_Dcuts_open _ _ Yr) ; apply hinhuniv ; intros q. generalize (pr1 (ispositive_minusNonnegativeRationals _ _) (pr2 (pr2 q))) ; intros Hq. generalize (is_Dcuts_corr Z _ Hq). apply hinhuniv ; apply sumofmaps ; [intros nZ | ]. + apply hinhpr ; left ; left. apply hinhpr. exists (pr1 q) ; split. * exact (pr1 (pr2 q)). * intros z ; apply sumofmaps ; [intros Zz | intros ->]. ** apply (minusNonnegativeRationals_ltcompat_l' _ _ r). rewrite plusNonnegativeRationals_minus_l. now apply (Dcuts_finite Z). ** now rewrite isrunit_zeroNonnegativeRationals ; apply_pr2 ispositive_minusNonnegativeRationals. + intros z. induction (isdecrel_leNonnegativeRationals r (pr1 z)) as [Hzr | Hzr]. * apply hinhpr ; left ; right. now apply (is_Dcuts_bot _ _ (pr1 (pr2 z))). * apply notge_ltNonnegativeRationals in Hzr ; apply lt_leNonnegativeRationals in Hzr. apply hinhpr ; right. exists (r - pr1 z ,, pr1 z) ; repeat split. ** simpl. now rewrite minusNonnegativeRationals_plus_r. ** apply hinhpr ; simpl. exists (pr1 q) ; split. { exact (pr1 (pr2 q)). } intros z' ; apply sumofmaps ; [intros Zz' | intros ->]. *** apply_pr2 (plusNonnegativeRationals_ltcompat_r (pr1 z)). rewrite isassoc_plusNonnegativeRationals, (iscomm_plusNonnegativeRationals z'), <- isassoc_plusNonnegativeRationals. rewrite minusNonnegativeRationals_plus_r. **** apply (minusNonnegativeRationals_ltcompat_l' _ _ r) ; rewrite plusNonnegativeRationals_minus_l. rewrite <- minusNonnegativeRationals_plus_exchange, iscomm_plusNonnegativeRationals. { apply (Dcuts_finite Z). - exact (pr2 (pr2 z)). - exact Zz'. } now apply lt_leNonnegativeRationals ; apply_pr2 ispositive_minusNonnegativeRationals. **** now apply Hzr. *** rewrite isrunit_zeroNonnegativeRationals. apply istrans_le_lt_ltNonnegativeRationals with r. **** now apply minusNonnegativeRationals_le. **** now apply_pr2 ispositive_minusNonnegativeRationals. ** exact (pr1 (pr2 z)). - apply hinhuniv ; apply sumofmaps ; [apply sumofmaps ; [ | intros Zr] | intros ryzz ; rewrite (pr1 (pr2 ryzz)) ]. + apply hinhuniv ; intros y. apply (is_Dcuts_bot _ _ (pr1 (pr2 y))). apply lt_leNonnegativeRationals. pattern r at 1 ; rewrite <- (isrunit_zeroNonnegativeRationals r). apply (pr2 (pr2 y)). now right. + now simple refine (Hyz _ _). + generalize (pr1 (pr2 (pr2 ryzz))) ; apply hinhuniv ; simpl ; intros y. apply (is_Dcuts_bot _ _ (pr1 (pr2 y))). apply lt_leNonnegativeRationals, (pr2 (pr2 y)). left. exact (pr2 (pr2 (pr2 ryzz))). 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.