LeftInverse plus_rng_localization negate_rng_localization zero_rng_localization. Proof. srapply Quotient_ind_hprop; intros f. apply qglue, fraction_eq_simple; simpl. refine (rng_mult_one_r _ @ _). refine (_ @ (rng_mult_zero_l _)^). rewrite rng_mult_negate_l. apply rng_plus_negate_l. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient