Lemma abgrdiffinvcomp (X : abmonoid) : iscomprelrelfun (hrelabgrdiff X) (eqrelabgrdiff X) (abgrdiffinvint X). 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'). exists (pr1 tt0). induction tt0 as [ a eq ]. change (s + x' + a = s' + x + a). 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. exact (!eq). Qed.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.