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.

Add Relation Qeq
reflexivity proved by Qeq_refl
symmetry proved by Qed_sym
transitivity proved by Qeq_trans
as qeq_rel.

I assume I have some kind of syntax error in my Add Relation. The generalized rewriting guide only brushes over the non-parametric kind of relation, so I didn’t get an example of it’s syntax.

Any hints to lead me to the right path?