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