Relation Fraction. Proof. intros [n1 d1 ?] [n2 d2 ?]. refine (exists (x : R), S x /\ _). exact (x * n1 * d2 = x * n2 * d1). Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient