Lemma islunit_Dcuts_plus_zero : islunit Dcuts_plus 0. Proof. intros x. apply Dcuts_eq_is_eq ; intro r ; split. - apply hinhuniv, sumofmaps. + apply sumofmaps ; intro Hr. * now apply Dcuts_zero_empty in Hr. * exact Hr. + intros x0. apply fromempty. exact (Dcuts_zero_empty _ (pr1 (pr2 (pr2 x0)))). - intros Hr. now apply hinhpr ; left ; right. 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.