rng_homo_crt x = (0, 1). Proof. apply rng_moveR_Mr in p. rewrite rng_plus_comm in p. apply path_prod; apply qglue. - change (I (-x + 0)). apply ideal_in_negate_plus. 1: assumption. apply ideal_in_zero. - change (J (-x + 1)). rewrite rng_plus_comm. by rewrite <- p. 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.