(I : Ideal R) : (ideal_unit R :: I) ↔ ideal_unit R. Proof. split. - cbn; trivial. - intros ?; split; apply tr; cbn; split; trivial. 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.