Lemma Dcuts_minus_correct_l: ∏ x y z : Dcuts, x = Dcuts_plus y z -> z = Dcuts_minus x y. Proof. intros _ Y Z ->. apply Dcuts_eq_is_eq ; intro r ; split. - intros Zr. generalize (is_Dcuts_open _ _ Zr) ; apply hinhuniv ; intros q. generalize (pr1 (ispositive_minusNonnegativeRationals _ _) (pr2 (pr2 q))) ; intros Hq. generalize (is_Dcuts_corr Y _ Hq) ; apply hinhuniv ; apply sumofmaps ; [intros nYy | ]. + apply hinhpr ; exists (pr1 q) ; split. * apply hinhpr ; left ; right. exact (pr1 (pr2 q)). * intros y ; apply sumofmaps ; [intros Yy | intros ->]. ** apply minusNonnegativeRationals_ltcompat_l' with r. rewrite plusNonnegativeRationals_minus_l. now apply (Dcuts_finite Y). ** rewrite isrunit_zeroNonnegativeRationals. now apply_pr2 ispositive_minusNonnegativeRationals. + intros y. apply hinhpr. exists (pr1 y + pr1 q) ; split. * apply hinhpr ; right ; exists (pr1 y,,pr1 q) ; simpl ; repeat split. ** exact (pr1 (pr2 y)). ** exact (pr1 (pr2 q)). * intros y' ; apply sumofmaps ; [intros Yy' | intros ->]. ** apply minusNonnegativeRationals_ltcompat_l' with r. rewrite plusNonnegativeRationals_minus_l. rewrite iscomm_plusNonnegativeRationals, <- minusNonnegativeRationals_plus_exchange, iscomm_plusNonnegativeRationals. *** apply (Dcuts_finite Y). **** exact (pr2 (pr2 y)). **** exact Yy'. *** now apply lt_leNonnegativeRationals ; apply_pr2 ispositive_minusNonnegativeRationals. ** rewrite isrunit_zeroNonnegativeRationals. apply istrans_lt_le_ltNonnegativeRationals with (pr1 q). *** now apply_pr2 ispositive_minusNonnegativeRationals. *** now apply plusNonnegativeRationals_le_l. - apply hinhuniv ; intros q. generalize (pr1 (pr2 q)) ; apply hinhuniv ; apply sumofmaps ; [ apply sumofmaps ; [intros Yq | intros Zq ] | intros yz ]. + apply fromempty, (isnonnegative_NonnegativeRationals' r). apply_pr2 (plusNonnegativeRationals_ltcompat_r (pr1 q)). rewrite islunit_zeroNonnegativeRationals. apply (pr2 (pr2 q)). now left. + apply is_Dcuts_bot with (1 := Zq), lt_leNonnegativeRationals. pattern r at 1 ; rewrite <- (isrunit_zeroNonnegativeRationals r). apply (pr2 (pr2 q)). now right. + apply is_Dcuts_bot with (1 := pr2 (pr2 (pr2 yz))), lt_leNonnegativeRationals. apply_pr2 (plusNonnegativeRationals_ltcompat_l (pr1 (pr1 yz))). rewrite <- (pr1 (pr2 yz)), iscomm_plusNonnegativeRationals. apply (pr2 (pr2 q)). left. exact (pr1 (pr2 (pr2 yz))). 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.