`{Univalence} {R : CRing} (I J : Ideal R) (c : Coprime I J) : R / (I ⋅ J)%ideal ≅ (R / I) × (R / J). Proof. etransitivity. { rapply rng_quotient_invar. symmetry. rapply ideal_intersection_is_product. } rapply chinese_remainder. 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.