proposition: Lemma abgrdiffinvcomp (X : abmonoid) : iscomprelrelfun (hrelabgrdiff X) (eqrelabgrdiff X) (abgrdiffinvint X).
proof: Proof. unfold iscomprelrelfun. unfold eqrelabgrdiff. unfold hrelabgrdiff. unfold eqrelabmonoidfrac. unfold hrelabmonoidfrac. simpl. intros xs xs'. apply (hinhfun). intro tt0. set (x := pr1 xs). set (s := pr2 xs). set (x' := pr1 xs'). set (s' := pr2 xs'). split with (pr1 tt0). destruct tt0 as [ a eq ]. change (paths (s + x' + a) (s' + x + a)). apply pathsinv0. simpl. set(e := commax X s' x). simpl in e. rewrite e. clear e. set (e := commax X s x'). simpl in e. rewrite e. clear e. apply eq. Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids