Lemma is_zero_dec : ∏ x : Dcuts, isboolDcuts x -> (x = 0) ∨ (¬ (x = 0)). Proof. intros x Hx. generalize (Hx 0%NRat) ; apply hinhfun ; apply sumofmaps ; intros Hx0. - right ; intro H. rewrite H in Hx0. now apply Dcuts_zero_empty in Hx0. - left ; apply Dcuts_eq_is_eq. split. + intros Hr. apply fromempty. apply Hx0. apply (is_Dcuts_bot x r). * now apply Hr. * apply isnonnegative_NonnegativeRationals. + intros Hr. now apply Dcuts_zero_empty in Hr. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.RealNumbers.NonnegativeRationals.