Build_IsSubring' {R : Ring} (S : R -> Type) (H : forall x, IsHProp (S x)) (H1 : forall x y, S x -> S y -> S (x - y)) (H2 : forall x y, S x -> S y -> S (x * y)) (H3 : S 1) : IsSubring S. Proof. snrapply Build_IsSubring. - snrapply Build_IsSubgroup'. + exact _. + pose (p := H1 1 1 H3 H3). rewrite rng_plus_negate_r in p. exact p. + exact H1. - exact H2. - exact H3. 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.