Definition abmonoidfrac_min : binop (abmonoidfrac X Y) := setquotfun2 (binopeqrelabmonoidfrac X Y) (binopeqrelabmonoidfrac X Y) _ (abmonoidfrac_lattice_def min Hmin).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.