Definition abmonoidfrac_latticewithgt (X : abmonoid) (Y : @submonoid X) (lat : latticewithgt X) (Hgt : ispartbinophrel Y (Lgt lat)) (Hop : ∏ (x : Y) (y z : X), y * pr1 x = z * pr1 x → y = z) (Hmin : ispartrdistr Y (Lmin lat) op) (Hmax : ispartrdistr Y (Lmax lat) op) : latticewithgt (abmonoidfrac X Y). Proof. simple refine (tpair _ _ _). refine (abmonoidfrac_lattice _ _ _ _ _). exact Hmin. exact Hmax. simple refine (tpair _ _ _). simple refine (StrongOrder_abmonoidfrac _ _ _). apply (Lgt lat). apply Hgt. split ; split. - apply abmonoidfrac_notgtle. apply notLgt_Lle. - apply abmonoidfrac_lenotgt. apply Lle_notLgt. apply Hop. - apply abmonoidfrac_gtmin. apply Lmin_Lgt. - apply abmonoidfrac_gtmax. apply Lmax_Lgt. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.