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