(f : Fraction) : class_of fraction_eq f = loc_in (numerator f) * inverse_elem (loc_in (denominator f)). Proof. apply qglue, fraction_eq_simple. nrapply rng_mult_assoc. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient