rng_localization_rec $o loc_in $== f. Proof. intros x; simpl. apply rng_inv_moveR_rV. lhs_V nrapply rng_mult_one_r. nrapply ap; symmetry. apply rng_homo_one. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient