Lemma Dcuts_of_Dcuts_corr: Dcuts_def_corr Dcuts_of_Dcuts_val. Proof. intros c Hc. apply ispositive_NQhalf in Hc. apply (pr2 (isapfun_NonnegativeRationals_to_Dcuts_aux _ _)) in Hc. generalize (E_corr _ Hc). apply isapfun_NonnegativeRationals_to_Dcuts_aux in Hc. apply hinhuniv ; apply sumofmaps ; [intros He | ]. - apply hinhpr ; left. use factor_through_squash. { exact isapropempty. } intros X. apply He. apply E_bot with (1 := pr1 (pr2 X)). intros r Hr. apply is_Dcuts_bot with c. { exact (pr2 (pr2 X)). } apply lt_leNonnegativeRationals. eapply istrans_lt_le_ltNonnegativeRationals. { exact Hr. } pattern c at 2 ; rewrite (NQhalf_double c). apply plusNonnegativeRationals_le_r. - apply hinhuniv ; intros X. generalize (is_Dcuts_corr (pr1 X) _ Hc). apply hinhfun ; apply sumofmaps ; [intros Xc | ]. + left. use factor_through_squash. { exact isapropempty. } intros Y. apply (pr2 (pr2 X)). apply E_bot with (1 := pr1 (pr2 Y)). apply Dcuts_lt_le_rel. apply hinhpr. exists c ; split. 2: exact (pr2 (pr2 Y)). intros H ; apply Xc. revert H ; apply hinhuniv ; apply sumofmaps ; [ apply sumofmaps ; [intros Xc' | intros Yc'] | ]. * apply is_Dcuts_bot with (1 := Xc'). pattern c at 2. rewrite (NQhalf_double c). apply plusNonnegativeRationals_le_r. * apply fromempty. revert Yc' ; simpl. change (¬ (c < c / 2)%NRat). apply (pr2 (notlt_geNonnegativeRationals _ _)). pattern c at 2. rewrite (NQhalf_double c). apply plusNonnegativeRationals_le_r. * intros xy. apply is_Dcuts_bot with (1 := pr1 (pr2 (pr2 xy))). apply_pr2 (plusNonnegativeRationals_lecompat_r (pr2 (pr1 xy))). rewrite <- (pr1 (pr2 xy)). pattern c at 2; rewrite (NQhalf_double c). apply plusNonnegativeRationals_lecompat_l. apply lt_leNonnegativeRationals. exact (pr2 (pr2 (pr2 xy))). + intro ; right. rename X0 into q. exists (pr1 q) ; split. * apply hinhpr. exists (pr1 X) ; split. ** exact (pr1 (pr2 X)). ** exact (pr1 (pr2 q)). * use factor_through_squash. { exact isapropempty. } intros Y. apply (pr2 (pr2 X)). apply E_bot with (1 := pr1 (pr2 Y)). intros r. apply hinhuniv ; apply sumofmaps. ** apply sumofmaps ; [intros Xc' | intros Yc' ]. *** apply is_Dcuts_bot with (1 := pr2 (pr2 Y)). pattern c at 1; rewrite (NQhalf_double c). rewrite <- isassoc_plusNonnegativeRationals. eapply istrans_leNonnegativeRationals, plusNonnegativeRationals_le_r. apply lt_leNonnegativeRationals. apply notge_ltNonnegativeRationals. intro ; apply (pr2 (pr2 q)). now apply is_Dcuts_bot with (1 := Xc'). *** apply is_Dcuts_bot with (1 := pr2 (pr2 Y)). pattern c at 1; rewrite (NQhalf_double c). rewrite <- isassoc_plusNonnegativeRationals. eapply istrans_leNonnegativeRationals, plusNonnegativeRationals_le_l. apply lt_leNonnegativeRationals. exact Yc'. ** intros xy. apply is_Dcuts_bot with (1 := pr2 (pr2 Y)). rewrite (pr1 (pr2 xy)). pattern c at 1; rewrite (NQhalf_double c). rewrite <- isassoc_plusNonnegativeRationals. eapply istrans_leNonnegativeRationals, plusNonnegativeRationals_lecompat_l. *** apply plusNonnegativeRationals_lecompat_r. apply lt_leNonnegativeRationals, notge_ltNonnegativeRationals. intro ; apply (pr2 (pr2 q)). now apply is_Dcuts_bot with (1 := pr1 (pr2 (pr2 xy))). *** apply lt_leNonnegativeRationals. exact (pr2 (pr2 (pr2 xy))). 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.