Lemma commringfracisinv1 (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : isinv (commringfracop1 X S) (commringfracunel1 X S) (commringfracinv1 X S). 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. exists (unel S). set (x := pr1 xs). set (s := pr1 (pr2 xs)). change ((s * (-1 * x) + s * x) * 1 * 1 = 0 * (s * s) * 1). induction (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)). exact (!ringmult0x X 1). } exact (isl ,, weqlinvrinv _ (commringfraccomm1 X S) _ (commringfracinv1 X S) isl). Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.