Lemma isdecrel_Lle_abmonoidfrac {X : abmonoid} (Y : @submonoid X) (lat : lattice X) (is' : isdecrel (Lle 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) : isdecrel (Lle (abmonoidfrac_lattice X Y lat Hmin Hmax)). Proof. refine (isdecrellogeqf _ _). - apply abmonoidfrac_Lle. - apply isdecabmonoidfracrel. split. + clear -Hmin Hop. intros x y z Hz ; rewrite !(commax X z) ; unfold Lle ; rewrite <- (Hmin _ _ (z,,Hz)) ; apply Hop. + clear -Hmin Hop. intros x y z Hz ; unfold Lle ; rewrite <- (Hmin _ _ (z,,Hz)) ; apply Hop. + apply is'. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.