R $-> rng_localization. Proof. snrapply Build_RingHomomorphism. 1: exact (class_of _ o frac_in). snrapply Build_IsSemiRingPreserving. - snrapply Build_IsMonoidPreserving. + intros x y. snrapply qglue. apply fraction_eq_simple. by simpl; rewrite 5 rng_mult_one_r. + reflexivity. - snrapply Build_IsMonoidPreserving. + intros x y. snrapply qglue. apply fraction_eq_simple. by simpl; rewrite 3 rng_mult_one_r. + reflexivity. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient