Definition Dcuts_ConstructiveCommutativeDivisionRig : ConstructiveCommutativeDivisionRig. Proof. exists Dcuts_commrig. exists (pr2 Dcuts). repeat split. - exact islapbinop_Dcuts_plus. - exact israpbinop_Dcuts_plus. - exact islapbinop_Dcuts_mult. - exact israpbinop_Dcuts_mult. - exact Dcuts_ap_one_zero. - intros x Hx. exists (Dcuts_inv x Hx) ; split. + exact (islinv_Dcuts_inv x Hx). + exact (isrinv_Dcuts_inv x Hx). 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.