Commutative mult_rng_localization. Proof. srapply Quotient_ind2_hprop; intros x y. apply qglue, fraction_eq_simple; simpl. f_ap; rapply rng_mult_comm. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient