Lemma isOneSided_Dcuts_bot : ∏ D, isOneSided D → Dcuts_def_bot (λ r, D (pr1 r)). Proof. intros D H r Dr q Hq. generalize (le_eqorltNonnegativeRationals _ _ Hq) ; clear Hq. apply sumofmaps ; intros H0. - rewrite H0. exact Dr. - rewrite ltNonnegativeRationals_correct in H0. generalize (pr2 (pr2 H) _ _ H0). apply hinhuniv, sumofmaps ; intros Dq. + exact Dq. + apply fromempty, Dq, Dr. Qed.
Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals. Require Import UniMath.RealNumbers.NonnegativeReals.