Lemma abgrdiffisinv (X : abmonoid) : isinv (@op (abgrdiffcarrier X)) 0 (abgrdiffinv X). Proof. set (R := eqrelabgrdiff X). assert (isl : islinv (@op (abgrdiffcarrier X)) 0 (abgrdiffinv X)). { unfold islinv. apply (setquotunivprop R (λ x, _ = _)%logic). intro xs. set (x := pr1 xs). set (s := pr2 xs). apply (iscompsetquotpr R (@op (abmonoiddirprod X X) (abgrdiffinvint X xs) xs) 0). simpl. apply hinhpr. exists (unel X). change (s + x + 0 + 0 = 0 + (x + s) + 0). induction (commax X x s). induction (commax X 0 (x + s)). apply idpath. } exact (isl ,, weqlinvrinv (@op (abgrdiffcarrier X)) (commax (abgrdiffcarrier X)) 0 (abgrdiffinv X) isl). Qed.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.