# Using Add Relation for Setoid equivalence of rationals

I like the build up the basic types such as Integers and rationals to understand how the Coq system works, and I’m trying to establish Setoid equivalence of the rationals, but I’m not sure quite how to tell the system that I’m doing that.

In the standard library for the rationals, it starts doing Instance stuff, which is something I have not learned yet, so I was trying to go back to what is in Generalized Rewriting in the manual https://coq.inria.fr/refman/addendum/generalized-rewriting.html.

I’ve established my proofs on reflexivity, symmetry and transitivity (trans was a lot harder to prove than the others).

Definition Qeq (r1 : rat) (r2 : rat) :=
match r1, r2 with
| Qmake i p, Qmake j q => times_int_pos i q = times_int_pos j p
end.

Lemma Qeq_refl : forall (r : rat), Qeq r r.
destruct r. simpl. reflexivity.
Qed.

Lemma Qeq_sym : forall (r s : rat), Qeq r s → Qeq s r.
destruct r; destruct s; intros H.
unfold Qeq in H. unfold Qeq. rewrite H.
reflexivity.
Qed.

Lemma Qeq_trans : forall (r s t : rat), Qeq r s → Qeq s t → Qeq r t.
details omitted
Qed.