Definition commringfracunit1 (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : ismonoidop (commringfracop1 X S) := commringfracassoc1 X S ,, commringfracunel1 X S ,, commringfraclunit1 X S ,, commringfracrunit1 X S.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.