proposition: Lemma Dcuts_minus_plus_r: ∏ x y z : Dcuts, z <= y -> x = Dcuts_minus y z -> y = Dcuts_plus x z.
proof: 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.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations UniMath.RealNumbers.Sets UniMath.Algebra.ConstructiveStructures UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim UniMath.RealNumbers.NonnegativeRationals