Lemma Dcuts_of_Dcuts'_bot : ∏ (x : Dcuts), Dcuts_of_Dcuts'_val x -> ∏ y : Dcuts, (y <= x) -> Dcuts_of_Dcuts'_val y. Proof. intros r Xr n Xn. revert Xr. apply hinhfun. intros q. exists (pr1 q). split. - intros Nq. apply (pr1 (pr2 q)). now simple refine (Xn _ _). - exact (pr2 (pr2 q)). 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.