Associative plus_rng_localization. Proof. srapply Quotient_ind3_hprop; intros x y z. apply qglue, fraction_eq_simple. simpl. rewrite ? rng_dist_r. rewrite ? rng_mult_assoc. rewrite ? rng_plus_assoc. do 4 f_ap. all: rewrite <- ? rng_mult_assoc. all: f_ap. 2: apply rng_mult_comm. rewrite rng_mult_assoc. apply rng_mult_comm. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient