Lemma abmonoidfrac_Lle (X : abmonoid) (Y : @submonoid X) (lat : lattice X) (Hmin : ispartrdistr Y (Lmin lat) op) (Hmax : ispartrdistr Y (Lmax lat) op) : ∏ x y : abmonoidfrac X Y, abmonoidfracrel X Y (ispartbinophrel_Lle X Y lat Hmin) x y <-> Lle (abmonoidfrac_lattice X Y lat Hmin Hmax) x y. Proof. simple refine (setquotuniv2prop _ (λ x y, _ ,, _) _). - apply isapropdirprod ; apply isapropimpl, propproperty. - intros x y. split. + apply abmonoidfrac_Lle_1. + apply abmonoidfrac_Lle_2. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.