fact: Definition commringop2axs (X : commring) : isabmonoidop (@op2 X) := tpair _ (ringop2axs X) (ringcomm2 X).
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids