Lemma commringfracinv1comp (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : iscomprelrelfun (eqrelcommringfrac X S) (eqrelcommringfrac X S) (commringfracinv1int X S). Proof. intros. set (assoc2 := ringassoc2 X). intros xs xs'. simpl. set (ff := @hinhfun). simpl in ff. apply ff. clear ff. intro tt0. exists (pr1 tt0). set (x := pr1 xs). set (s := pr1 (pr2 xs)). set (x' := pr1 xs'). set (s' := pr1 (pr2 xs')). set (a0 := pr1 (pr1 tt0)). change (-1 * x * s' * a0 = -1 * x' * s * a0). rewrite (assoc2 -1 x s'). rewrite (assoc2 -1 x' s). rewrite (assoc2 -1 (x * s') a0). rewrite (assoc2 -1 (x' * s) a0). apply (maponpaths (λ x0 : X, -1 * x0) (pr2 tt0)). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.