(I J : Ideal R) : I ⊆ J -> J :: I ↔ ideal_unit R. Proof. intros p. apply ideal_subset_antisymm. 1: cbv; trivial. intros r _; split; apply tr; intros x q; cbn. - by apply isleftideal, p. - rapply isrightideal. by apply p. 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.