Build_Subring' {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) : Subring R := Build_Subring R S (Build_IsSubring' S H H1 H2 H3). Coercion subgroup_subring {R} : Subring R -> Subgroup R := fun S => Build_Subgroup R S _. Coercion ring_subring {R : Ring} (S : Subring R) : Ring. Proof. snrapply (Build_Ring (subgroup_subring S)). 3-7: hnf; intros; srapply path_sigma_hprop. - intros [r ?] [s ?]; exists (r * s). by apply issubring_mult. - exists 1. apply issubring_one. - snrapply rng_mult_assoc. - snrapply rng_dist_l. - snrapply rng_dist_r. - snrapply rng_mult_one_l. - snrapply rng_mult_one_r. 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.