proposition: Lemma rng_homo_crt_beta_left : rng_homo_crt x = (0, 1).
proof: 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.
imports: Classes.interfaces.abstract_algebra WildCat Modalities.ReflectiveSubuniverse Algebra.AbGroups Algebra.Rings.CRing Algebra.Rings.Ideal Algebra.Rings.QuotientRing