Lemma Dcuts_min_corr : Dcuts_def_corr Dcuts_min_val. 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.
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.