R $-> (R / I) × (R / J). Proof. apply ring_product_corec. 1,2: apply rng_quotient_map. Defined.
Require Import Classes.interfaces.canonical_names. Require Import WildCat. Require Import Modalities.ReflectiveSubuniverse. Require Import Algebra.AbGroups. Require Import Algebra.Rings.Ring. Require Import Algebra.Rings.Ideal. Require Import Algebra.Rings.QuotientRing. Require Import Algebra.Rings.CRing. Import Ideal.Notation.