Definition Dcuts_commrig : commrig. Proof. exists Dcuts_setwith2binop. repeat split. - exists (isabmonoidop_Dcuts_plus,,ismonoidop_Dcuts_mult). split. + exact islabsorb_Dcuts_mult_zero. + exact israbsorb_Dcuts_mult_zero. - exact isldistr_Dcuts_plus_mult. - exact isrdistr_Dcuts_plus_mult. - exact iscomm_Dcuts_mult. Defined.
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.