Definition commringfrac (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : commring. Proof. intros. set (R := eqrelcommringfrac X S). set (mult1 := commringfracop2 X S). set (add1 := commringfracop1 X S). set (uset := setquotinset R). apply (commringconstr add1 mult1). - exists (commringfracunit1 X S). exists (commringfracinv1 X S). apply (commringfracisinv1 X S). - apply (commringfraccomm1 X S). - apply (pr2 (abmonoidfrac (ringmultabmonoid X) S)). - apply (commringfraccomm2 X S). - apply (commringfracldistr X S ,, commringfracrdistr X S). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.