Lemma isrunit_Dcuts_plus_zero : isrunit Dcuts_plus 0. Proof. intros x. rewrite iscomm_Dcuts_plus. now apply islunit_Dcuts_plus_zero. 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.