proposition: Lemma isOneSided_Dcuts_bot : ∏ D, isOneSided D → Dcuts_def_bot (λ r, D (pr1 r)).
proof: 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.
imports: UniMath.NumberSystems.RationalNumbers UniMath.RealNumbers.Prelim UniMath.RealNumbers.NonnegativeRationals UniMath.RealNumbers.NonnegativeReals