proposition: Lemma isdeceqabmonoidfrac (X : abmonoid) (A : submonoid X) (iscanc : ∏ a : A, isrcancelable (@op X) (pr1carrier _ a)) (is : isdeceq X) : isdeceq (abmonoidfrac X A).
proof: 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.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders