{R : Ring} (I J : Subgroup R) := (forall x, I x -> J x). Global Instance reflexive_ideal_subset {R : Ring} : Reflexive (@ R) := fun _ _ => idmap. Global Instance transitive_ideal_subset {R : Ring} : Transitive (@ R). Proof. intros x y z p q a. exact (q a o p a). 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.