proposition: 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: Proof. refine (istotallogeqf _ _). - apply abmonoidfrac_Lle. - apply istotalabmonoidfracrel, is'. Qed.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Groups