proposition: Lemma Dcuts_plus_ltcompat_l : ∏ x y z: Dcuts, (y < z) <-> (Dcuts_plus y x < Dcuts_plus z x).
proof: Proof. intros x y z. split. - apply hinhuniv ; intros r. generalize (is_Dcuts_open _ _ (pr2 (pr2 r))) ; apply hinhuniv ; intros r'. generalize (pr1 r') (pr1 (pr2 r')) (pr2 (pr2 r')) ; clear r' ; intros r' Zr' Hr. apply ispositive_minusNonnegativeRationals in Hr. generalize (is_Dcuts_corr x _ Hr). apply hinhuniv ; apply sumofmaps ; [intros nXc | ]. + apply hinhpr ; exists r' ; split. * unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; apply sumofmaps ; [apply sumofmaps ; [intros Yr' | intros Xr'] | intros yx ]. ** apply (pr1 (pr2 r)), is_Dcuts_bot with (1 := Yr'), lt_leNonnegativeRationals. now apply_pr2 ispositive_minusNonnegativeRationals. ** apply nXc, is_Dcuts_bot with (1 := Xr'), minusNonnegativeRationals_le. ** generalize (pr1 (pr2 yx)) ; apply gtNonnegativeRationals_noteq. pattern r' at 1 ; rewrite <- (minusNonnegativeRationals_plus_r (pr1 r) r'), iscomm_plusNonnegativeRationals. *** apply plusNonnegativeRationals_ltcompat. { apply (Dcuts_finite y). { exact (pr1 (pr2 r)). } exact (pr1 (pr2 (pr2 yx))). } apply (Dcuts_finite x). { exact nXc. } exact (pr2 (pr2 (pr2 yx))). *** apply lt_leNonnegativeRationals. now apply_pr2 ispositive_minusNonnegativeRationals. * now apply hinhpr ; left ; left. + intros q. generalize (pr1 q) (pr1 (pr2 q)) (pr2 (pr2 q)) ; clear q ; intros q Xq nXq. apply hinhpr. exists (r' + q)%NRat ; split. * unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; apply sumofmaps ; [ apply sumofmaps ; [ intros Yr' | intros Xr'] | intros yx ]. ** apply (pr1 (pr2 r)), is_Dcuts_bot with (1 := Yr'), lt_leNonnegativeRationals. rewrite <- (isrunit_zeroNonnegativeRationals (pr1 r)). apply plusNonnegativeRationals_lt_le_ltcompat. *** now apply_pr2 ispositive_minusNonnegativeRationals. *** now apply isnonnegative_NonnegativeRationals. ** apply nXq, is_Dcuts_bot with (1 := Xr'). rewrite iscomm_plusNonnegativeRationals. apply plusNonnegativeRationals_lecompat_r. now apply minusNonnegativeRationals_le. ** generalize (pr1 (pr2 yx)) ; apply gtNonnegativeRationals_noteq. pattern (r' + q) at 1 ; rewrite (iscomm_plusNonnegativeRationals r' q). pattern r' at 1 ; rewrite <- (minusNonnegativeRationals_plus_r (pr1 r) r'), <- isassoc_plusNonnegativeRationals, iscomm_plusNonnegativeRationals. *** apply plusNonnegativeRationals_ltcompat. **** apply (Dcuts_finite y). { exact (pr1 (pr2 r)). } exact (pr1 (pr2 (pr2 yx))). **** apply (Dcuts_finite x). { exact nXq. } exact (pr2 (pr2 (pr2 yx))). *** apply lt_leNonnegativeRationals. now apply_pr2 ispositive_minusNonnegativeRationals. * apply hinhpr ; right ; exists (r',,q) ; repeat split. ** exact Zr'. ** exact Xq. - now apply Dcuts_plus_lt_l. 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