Definition abmonoidfrac_lattice (X : abmonoid) (Y : @submonoid X) (lat : lattice X) (Hmin : ispartrdistr Y (Lmin lat) op) (Hmax : ispartrdistr Y (Lmax lat) op) : lattice (abmonoidfrac X Y). Proof. exists (abmonoidfrac_min X Y Hmin). exists (abmonoidfrac_max X Y Hmax). apply abmonoidfrac_islatticeop. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.