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