proposition: Lemma 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: 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.
imports: Classes.interfaces.abstract_algebra WildCat Modalities.ReflectiveSubuniverse Algebra.AbGroups Algebra.Rings.CRing Algebra.Rings.Ideal Algebra.Rings.QuotientRing