proposition: Lemma ideal_quotient_trivial (I J : Ideal R) : I ⊆ J -> J :: I ↔ ideal_unit R.
proof: Proof. intros p. apply ideal_subset_antisymm. 1: cbv; trivial. intros r _ x q. by apply isideal, p. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups