Lemma Dcuts_of_Dcuts'_corr: ∏ c : Dcuts, 0 < c -> (¬ Dcuts_of_Dcuts'_val c) ∨ (hexists (λ P, Dcuts_of_Dcuts'_val P × ¬ Dcuts_of_Dcuts'_val (Dcuts_plus P c))). Proof. intros C HC. assert (∃ c : NonnegativeRationals, c ∈ C × (0 < c)%NRat). { revert HC ; apply hinhuniv ; intro d. generalize (is_Dcuts_open _ _ (pr2 (pr2 d))). apply hinhfun. intro c. exists (pr1 c). split. - exact (pr1 (pr2 c)). - eapply istrans_le_lt_ltNonnegativeRationals, (pr2 (pr2 c)). now apply isnonnegative_NonnegativeRationals. } revert X ; apply hinhuniv ; intros c. generalize (E_corr _ (pr2 (pr2 c))). apply hinhfun. apply sumofmaps ; [intros Ec | intros q]. - left. use factor_through_squash. { exact isapropempty. } intros r. apply Ec. apply E_bot with (1 := (pr2 (pr2 r))). apply lt_leNonnegativeRationals, notge_ltNonnegativeRationals. intro H. apply (pr1 (pr2 r)). now apply is_Dcuts_bot with (1 := pr1 (pr2 c)). - right. apply hinhpr. exists (NonnegativeRationals_to_Dcuts (pr1 q)). split. + apply hinhpr. exists (pr1 q). split. * simpl. apply isirrefl_ltNonnegativeRationals. * exact (pr1 (pr2 q)). + intro H ; apply (pr2 (pr2 q)). revert H. apply hinhuniv. intros r. apply E_bot with (1 := (pr2 (pr2 r))). apply notlt_geNonnegativeRationals. intro H. apply (pr1 (pr2 r)). generalize (isdecrel_ltNonnegativeRationals (pr1 r) (pr1 c)) ; apply sumofmaps ; intros H0. * apply hinhpr. left. right. apply is_Dcuts_bot with (1 := pr1 (pr2 c)). now apply lt_leNonnegativeRationals. * apply notlt_geNonnegativeRationals in H0. apply hinhpr. right. exists ((pr1 r - pr1 c)%NRat,, pr1 c). simpl ; split ; [ | split]. ** now apply pathsinv0, minusNonnegativeRationals_plus_r. ** apply_pr2 (plusNonnegativeRationals_ltcompat_r (pr1 c)). now rewrite minusNonnegativeRationals_plus_r. ** exact (pr1 (pr2 c)). 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.