Lemma isapropissubring {X : ring} (A : hsubtype X) : isaprop (issubring A). Proof. intros. apply (isofhleveldirprod 1). - apply isapropissubgr. - apply isapropissubmonoid. Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.