LeftIdentity plus_rng_localization zero_rng_localization. Proof. srapply Quotient_ind_hprop; intros f. apply qglue, fraction_eq_simple; simpl. f_ap. - rewrite rng_mult_zero_l. rewrite rng_plus_zero_l. apply rng_mult_one_r. - symmetry. apply rng_mult_one_l. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient