fact: Definition rigmultx0 (X : rig) : ∏ x : X, paths (op2 x (@rigunel1 X)) (@rigunel1 X) := rigmultx0_is (pr2 X).
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids