Lemma abmonoidfrac_Lle_2 (X : abmonoid) (Y : @submonoid X) (lat : lattice X) (Hmin : ispartrdistr _ (Lmin lat) op) : ∏ (x y : abmonoiddirprod X _), abmonoidfrac_min X Y Hmin (setquotpr (binopeqrelabmonoidfrac X Y) x) (setquotpr (binopeqrelabmonoidfrac X Y) y) = setquotpr (binopeqrelabmonoidfrac X Y) x → abmonoidfracrel X Y (ispartbinophrel_Lle X Y lat Hmin) (setquotpr (binopeqrelabmonoidfrac X Y) x) (setquotpr (binopeqrelabmonoidfrac X Y) y). Proof. intros x y. unfold abmonoidfracrel, quotrel, abmonoidfrac_min. rewrite setquotuniv2comm, setquotfun2comm. intros H. generalize (invmap (weqpathsinsetquot _ _ _) H). apply hinhfun. simpl. intros c. exists (pr2 x * pr1 c). rewrite <- Hmin. change (pr1 (pr2 x * pr1 c))%multmonoid with (pr1 (pr2 x) * pr1 (pr1 c))%multmonoid. rewrite <- assocax. refine (pathscomp0 _ _). apply (pr2 c). do 3 rewrite (assocax X) ; apply maponpaths. rewrite commax, assocax. apply maponpaths. apply commax. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.