proposition: Lemma is_zero_dec : ∏ x : Dcuts, isboolDcuts x -> (x = 0) ∨ (¬ (x = 0)).
proof: 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.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.RealNumbers.Prelim UniMath.RealNumbers.Sets UniMath.RealNumbers.NonnegativeRationals UniMath.RealNumbers.NonnegativeReals