proposition: Lemma commringfracisinv1 (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : isinv (commringfracop1 X S) (commringfracunel1 X S) (commringfracinv1 X S).
proof: Proof. intros. assert (isl : islinv (commringfracop1 X S) (commringfracunel1 X S) (commringfracinv1 X S)). { set (R := eqrelcommringfrac X S). set (add1int := commringfracop1int X S). set (add1 := commringfracop1 X S). set (inv1 := commringfracinv1 X S). set (inv1int := commringfracinv1int X S). set (qunel1int := commringfracunel1int X S). set (qunel1 := commringfracunel1 X S). set (assoc2 := ringassoc2 X). unfold islinv. apply (setquotunivprop _ (λ x, _ = _)). intro xs. apply (iscompsetquotpr R (add1int (inv1int xs) xs) qunel1int). simpl. apply hinhpr. split with (unel S). set (x := pr1 xs). set (s := pr1 (pr2 xs)). change (paths ((s * (-1 * x) + s * x) * 1 * 1) (0 * (s * s) * 1)). destruct (ringldistr X (-1 * x) x s). rewrite (ringmultwithminus1 X x). rewrite (ringlinvax1 X x). rewrite (ringmultx0 X s). rewrite (ringmult0x X 1). rewrite (ringmult0x X 1). rewrite (ringmult0x X (s * s)). apply (pathsinv0 (ringmult0x X 1)). } apply (make_dirprod isl (weqlinvrinv (commringfracop1 X S) (commringfraccomm1 X S) (commringfracunel1 X S) (commringfracinv1 X S) isl)). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids