Commutative plus_rng_localization. Proof. srapply Quotient_ind2_hprop; intros x y. apply qglue, fraction_eq_simple; simpl. rewrite (rng_mult_comm (denominator y) (denominator x)). f_ap; apply rng_plus_comm. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient