Definition abmonoidfrac_latticedec {X : abmonoid} (Y : @submonoid X) (lat : latticedec X) (Hop : ∏ (x : Y) (y z : X), y * pr1 x = z * pr1 x → y = z) (Hmin : ispartrdistr Y (Lmin lat) op) (Hmax : ispartrdistr Y (Lmax lat) op) : latticedec (abmonoidfrac X Y). Proof. exists (abmonoidfrac_lattice X Y lat Hmin Hmax). split. - apply istotal_Lle_abmonoidfrac. apply istotal_latticedec. - apply isdecrel_Lle_abmonoidfrac. + apply isdecrel_latticedec. + apply Hop. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.