Lemma Dcuts_def_corr_finite (X : hsubtype NonnegativeRationals) : Dcuts_def_corr X → Dcuts_def_finite X. Proof. intros Hx. specialize (Hx _ ispositive_oneNonnegativeRationals). revert Hx ; apply hinhuniv ; apply sumofmaps ; [intros Hx | intros x]. - apply hinhpr. exists 1 ; exact Hx. - apply hinhpr ; exists (pr1 x + 1) ; exact (pr2 (pr2 x)). 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.