{R : Ring} (S : R -> Type) : Subgroup R. Proof. snrapply Build_Subgroup'. - exact (fun r => merely (forall x, S x -> r * x = ring_zero)). - exact _. - apply tr. intros r p. apply rng_mult_zero_l. - intros x y p q. strip_truncations; apply tr. intros r s. lhs rapply rng_dist_r. rewrite (p r s). rewrite rng_mult_negate_l. rewrite (q r s). rewrite <- rng_mult_negate. rewrite rng_mult_zero_r. apply left_identity. Defined.
Require Import Basics Types. Require Import Spaces.Finite.Fin. Require Import Classes.interfaces.canonical_names. Require Import Algebra.Rings.Ring. Require Import Algebra.Groups.Subgroup. Require Import Algebra.AbGroups. Require Import WildCat.Core. Module Import Notation.