Associative mult_rng_localization. Proof. srapply Quotient_ind3_hprop; intros x y z. apply qglue, fraction_eq_simple. f_ap; [|symmetry]; apply rng_mult_assoc. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient