proposition: Lemma islunit_Dcuts_plus_zero : islunit Dcuts_plus 0.
proof: 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.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations UniMath.RealNumbers.Sets UniMath.Algebra.ConstructiveStructures UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim UniMath.RealNumbers.NonnegativeRationals