proposition: Lemma rng_homo_crt_beta_right : rng_homo_crt y = (1, 0).
proof: Proof. apply rng_moveR_rM in p. rewrite rng_plus_comm in p. apply path_prod; apply qglue. - change (I (-y + 1)). by rewrite <- p. - change (J (-y + 0)). apply ideal_in_negate_plus. 1: assumption. apply ideal_in_zero. Defined.
imports: Classes.interfaces.abstract_algebra WildCat Modalities.ReflectiveSubuniverse Algebra.AbGroups Algebra.Rings.CRing Algebra.Rings.Ideal Algebra.Rings.QuotientRing