(f1 f1' f2 f2' : Fraction) (p : fraction_eq f1 f1') (q : fraction_eq f2 f2') : fraction_eq (frac_add f1 f2) (frac_add f1' f2'). Proof. destruct f1 as [a s ss], f1' as [a' s' ss'], f2 as [b t st], f2' as [b' t' st'], p as [x [sx p]], q as [y [sy q]]. refine (x * y ; (mss_mult sx sy, _)). simpl. rewrite 2 rng_dist_l, 2 rng_dist_r. snrapply (ap011 (+)). - rewrite 4 rng_mult_assoc. rewrite 8 (rng_mult_permute_2_3 _ y). apply (ap (.* y)). rewrite 2 (rng_mult_permute_2_3 _ t). apply (ap (.* t)). rewrite (rng_mult_permute_2_3 _ t'). f_ap. - do 2 lhs_V nrapply rng_mult_assoc. do 2 rhs_V nrapply rng_mult_assoc. f_ap. rewrite 6 rng_mult_assoc. rewrite 2 (rng_mult_permute_2_3 _ _ t'). rewrite 2 (rng_mult_permute_2_3 _ _ t). lhs_V nrapply rng_mult_assoc. rhs_V nrapply rng_mult_assoc. f_ap; apply rng_mult_comm. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient