proposition: Lemma commringfracinv1comp (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : iscomprelrelfun (eqrelcommringfrac X S) (eqrelcommringfrac X S) (commringfracinv1int X S).
proof: Proof. intros. set (assoc2 := ringassoc2 X). intros xs xs'. simpl. set (ff := @hinhfun). simpl in ff. apply ff. clear ff. intro tt0. split with (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 (paths (-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.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids