Lemma isdeceqabmonoidfrac (X : abmonoid) (A : submonoid X) (iscanc : ∏ a : A, isrcancelable (@op X) (pr1carrier _ a)) (is : isdeceq X) : isdeceq (abmonoidfrac X A). Proof. apply (isdeceqsetquot (eqrelabmonoidfrac X A)). intros xa xa'. apply (isdecpropweqb (weqhrelhrel0abmonoidfrac X A iscanc xa xa')). apply isdecpropif. unfold isaprop. simpl. set (int := setproperty X (pr1 xa + pr1 (pr2 xa')) (pr1 xa' + pr1 (pr2 xa))). simpl in int. apply int. unfold hrel0abmonoidfrac. simpl. apply (is _ _). Defined.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.