f1 f2 f2' (p : fraction_eq f2 f2') : fraction_eq (frac_mult f1 f2) (frac_mult f1 f2'). Proof. destruct p as [x [s p]]. refine (x; (s, _)); simpl. rewrite 4 rng_mult_assoc. rewrite (rng_mult_permute_2_3 _ _ (numerator f2)). rewrite 2 (rng_mult_permute_2_3 _ _ (denominator f2')). rewrite (rng_mult_permute_2_3 _ _ (numerator f2')). rewrite 2 (rng_mult_permute_2_3 _ _ (denominator f2)). lhs_V nrapply rng_mult_assoc. rhs_V nrapply rng_mult_assoc. f_ap. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient