Lemma abmonoidfrac_islatticeop (X : abmonoid) (Y : @submonoid X) (lat : lattice X) : ∏ (Hmin : ispartrdistr Y (Lmin lat) op) (Hmax : ispartrdistr Y (Lmax lat) op), islatticeop (abmonoidfrac_min X Y Hmin) (abmonoidfrac_max X Y Hmax). Proof. intros Hmin Hmax. repeat split. - apply isassoc_abmonoidfrac_min, isassoc_Lmin. - apply iscomm_abmonoidfrac_min, iscomm_Lmin. - apply isassoc_abmonoidfrac_max, isassoc_Lmax. - apply iscomm_abmonoidfrac_max, iscomm_Lmax. - apply isabsorb_abmonoidfrac_min_max, Lmin_absorb. - apply isabsorb_abmonoidfrac_max_min, Lmax_absorb. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.