Plus (Quotient fraction_eq). Proof. srapply Quotient_rec2. - cbn. intros f1 f2. exact (class_of _ (frac_add f1 f2)). - intros f1 f1' f2 p. by apply qglue, frac_add_wd_l. - intros f1 f2 f2' q. by apply qglue, frac_add_wd_r. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient