f1 f2 (p : numerator f1 * denominator f2 = numerator f2 * denominator f1) : fraction_eq f1 f2. Proof. exists 1. refine (mss_one, _). lhs_V nrapply rng_mult_assoc. rhs_V nrapply rng_mult_assoc. exact (ap (1 *.) p). Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient