proposition: Lemma isapropissubrig {X : rig} (A : hsubtype X) : isaprop (issubrig A).
proof: Proof. intros. apply (isofhleveldirprod 1). - apply isapropissubmonoid. - apply isapropissubmonoid. Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids