proposition: Lemma Dcuts_min_corr : Dcuts_def_corr Dcuts_min_val.
proof: Proof. intros c Hc0. generalize (X_corr _ Hc0) (Y_corr _ Hc0) ; apply hinhfun2 ; apply (sumofmaps (Z := _ → _)) ; [intros nXc | intros q] ; intros Hy. - left ; intros Hc. apply nXc. exact (pr1 Hc). - revert Hy ; apply sumofmaps ; [intros nYc | intros q']. + left ; intros Hc. apply nYc. exact (pr2 Hc). + right. generalize (isdecrel_ltNonnegativeRationals (pr1 q) (pr1 q')) ; apply sumofmaps ; intros H. * exists (pr1 q) ; repeat split. ** exact (pr1 (pr2 q)). ** apply Y_bot with (1 := pr1 (pr2 q')), lt_leNonnegativeRationals, H. ** intros Hc. apply (pr2 (pr2 q)). exact (pr1 Hc). * exists (pr1 q') ; repeat split. ** apply X_bot with (1 := pr1 (pr2 q)), notlt_geNonnegativeRationals, H. ** exact (pr1 (pr2 q')). ** intros Hc. apply (pr2 (pr2 q')). exact (pr2 Hc). 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