issurjection_rng_homo_crt' (x y : R) (q1 : rng_homo_crt x = (0, 1)) (q2 : rng_homo_crt y = (1, 0)) : IsSurjection rng_homo_crt. Proof. intros [a b]. revert a; srapply QuotientRing_ind_hprop; intro a. revert b; srapply QuotientRing_ind_hprop; intro b. snrapply Build_Contr; [|intros z; strip_truncations; apply path_ishprop]. apply tr; exists (b * x + a * y). rewrite rng_homo_plus. rewrite 2 rng_homo_mult. rewrite q1, q2. apply path_prod. + change ([b] * 0 + [a] * 1 = [a] :> R / I). by rewrite rng_mult_one_r, rng_mult_zero_r, rng_plus_zero_l. + change ([b] * 1 + [a] * 0 = [b] :> R / J). by rewrite rng_mult_one_r, rng_mult_zero_r, rng_plus_zero_r. 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.