proposition: Lemma ideal_sum_subset_r (I J : Ideal R) : J ⊆ (I + J).
proof: Proof. intros x p. apply tr, sgt_in. right; exact p. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups