Build_Subring'' {R : Ring} (S : Subgroup R) (H1 : forall x y, S x -> S y -> S (x * y)) (H2 : S 1) : Subring R. Proof. snrapply (Build_Subring _ S). snrapply Build_IsSubring. - exact _. - exact H1. - exact H2. Defined.
Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Nat.Arithmetic. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.Groups.Group Algebra.Groups.Subgroup. Require Import Modalities.ReflectiveSubuniverse.