proposition: Lemma abgrdiffisinv (X : abmonoid) : isinv (@op (abgrdiffcarrier X)) (unel (abgrdiffcarrier X)) (abgrdiffinv X).
proof: Proof. set (R := eqrelabgrdiff X). assert (isl : islinv (@op (abgrdiffcarrier X)) (unel (abgrdiffcarrier X)) (abgrdiffinv X)). { unfold islinv. apply (setquotunivprop R (λ x, _ = _)). intro xs. set (x := pr1 xs). set (s := pr2 xs). apply (iscompsetquotpr R (@op (abmonoiddirprod X X) (abgrdiffinvint X xs) xs) (unel _)). simpl. apply hinhpr. split with (unel X). change (paths (s + x + (unel X) + (unel X)) ((unel X) + (x + s) + (unel X))). destruct (commax X x s). destruct (commax X (unel X) (x + s)). apply idpath. } apply (make_dirprod isl (weqlinvrinv (@op (abgrdiffcarrier X)) (commax (abgrdiffcarrier X)) (unel (abgrdiffcarrier X)) (abgrdiffinv X) isl)). Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids