fact: Definition commringfracinv1int (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : dirprod X S -> dirprod X S := λ xs : _, make_dirprod ((-1) * (pr1 xs)) (pr2 xs).
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids