proposition: Lemma Dcuts_minus_correct_l: ∏ x y z : Dcuts, x = Dcuts_plus y z -> z = Dcuts_minus x y.
proof: 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.
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