rng_localization -> T. Proof. srapply Quotient_rec. - intros [n d sd]. refine (f n * inverse_elem (f d)). exact (H d sd). - simpl. intros x y z. apply rng_inv_moveR_rV. rhs_V nrapply rng_mult_move_left_assoc. rhs_V nrapply rng_mult_assoc. apply rng_inv_moveL_Vr. lhs_V nrapply rng_homo_mult. rhs_V nrapply rng_homo_mult. nrapply (equiv_inj (f z.1 *.)). { nrapply isequiv_rng_inv_mult_l. exact (H _ (fst z.2)). } lhs_V nrapply rng_homo_mult. rhs_V nrapply rng_homo_mult. lhs nrapply ap. 1: lhs nrapply rng_mult_assoc. 1: nrapply rng_mult_permute_2_3. rhs nrapply ap. 2: nrapply rng_mult_assoc. exact (ap f (snd z.2)). Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient