Lemma isdeceqcommringfrac (X : commring) (S : @submonoid (ringmultabmonoid X)) (iscanc : ∏ a : S, isrcancelable (@op2 X) (pr1carrier _ a)) (is : isdeceq X) : isdeceq (commringfrac X S). Proof. intros. apply (isdeceqsetquot (eqrelcommringfrac X S)). intros xa xa'. apply (isdecpropweqb (weqhrelhrel0commringfrac X S 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 hrelcommringfrac0. simpl. apply (is _ _). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.