fact: Definition pr1subrig (X : rig) : @subrig X -> hsubtype X := @pr1 _ (λ A : hsubtype X, issubrig A).
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids