LeftIdentity mult_rng_localization one_rng_localization. Proof. srapply Quotient_ind_hprop; intros f. apply qglue, fraction_eq_simple; simpl. f_ap; [|symmetry]; apply rng_mult_one_l. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient