Definition addsubgr {X : ring} : subring X → @subgr X := λ A, @make_subgr X (pr1 A) (pr1 (pr2 A)).
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.