fact: Definition rigtoringisunit (X : rig) : isunit (rigtoringop2 X) (rigtoringunel2 X) := make_dirprod (rigtoringlunit2 X) (rigtoringrunit2 X).
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids