IsSemiRingPreserving rng_localization_rec_map. Proof. snrapply Build_IsSemiRingPreserving. - snrapply Build_IsMonoidPreserving. + srapply Quotient_ind2_hprop. intros x y; simpl. apply rng_inv_moveR_rV. rhs nrapply rng_dist_r. rewrite rng_homo_plus. rewrite 3 rng_homo_mult. f_ap. 1,2: rhs_V nrapply rng_mult_assoc. 1,2: f_ap. 1,2: lhs_V nrapply rng_mult_one_l. 1,2: rhs nrapply rng_mult_assoc. 2: rhs nrapply rng_mult_comm. 2: rhs nrapply rng_mult_assoc. 1,2: f_ap. 1,2: symmetry. * apply rng_inv_l. * apply rng_inv_r. + hnf; simpl. rewrite rng_homo_zero. nrapply rng_mult_zero_l. - snrapply Build_IsMonoidPreserving. + srapply Quotient_ind2_hprop. intros x y; simpl. apply rng_inv_moveR_rV. lhs nrapply rng_homo_mult. rhs_V nrapply rng_mult_assoc. rhs_V nrapply rng_mult_assoc. apply ap. apply rng_inv_moveL_Vr. lhs nrapply rng_mult_comm. rhs_V nrapply rng_mult_assoc. apply ap. apply rng_inv_moveL_Vr. symmetry. rhs nrapply rng_mult_comm. nrapply rng_homo_mult. + apply rng_inv_moveR_rV; symmetry. apply rng_mult_one_l. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient