proposition: Lemma ideal_zero_subset I : ideal_zero R ⊆ I.
proof: Proof. intros x p; rewrite p; apply ideal_in_zero. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups