Lemma istotal_Lle_abmonoidfrac {X : abmonoid} (Y : @submonoid X) (lat : lattice X) (is' : istotal (Lle lat)) (Hmin : ispartrdistr Y (Lmin lat) op) (Hmax : ispartrdistr Y (Lmax lat) op) : istotal (Lle (abmonoidfrac_lattice X Y lat Hmin Hmax)). Proof. refine (istotallogeqf _ _). - apply abmonoidfrac_Lle. - apply istotalabmonoidfracrel, is'. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.