{R S : Ring} (f : R $-> S) : Subring S. Proof. snrapply (Build_Subring'' (grp_image f)). - simpl. intros x y p q. strip_truncations; apply tr. destruct p as [a p'], q as [b q']. exists (a * b). refine (rng_homo_mult _ _ _ @ _). f_ap. - apply tr. exists 1. exact (rng_homo_one f). 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.