Feature Request: setoid_rewrite should possibly work better with PERs

Version

8.8.1

Description of the problem

Given a partial equivalence relation R, if we know R x y for any y, then we know Proper R x. I ran into a situation where I had R x y in the context, and thought that setoid_rewrite did not work with PERs because of this. I then discovered it does. It might be useful to automatically support this use case, which could be accomplished by adding the following hints to typeclass_instances:

Require Import Coq.Classes.Morphisms.
Require Import Coq.Setoids.Setoid.

Lemma PER_valid_l {A} {R : relation A} {HS : Symmetric R} {HT : Transitive R} x y (H : R x y) : Proper R x.
Proof. hnf; etransitivity; eassumption || symmetry; eassumption. Qed.
Lemma PER_valid_r {A} {R : relation A} {HS : Symmetric R} {HT : Transitive R} x y (H : R x y) : Proper R y.
Proof. hnf; etransitivity; eassumption || symmetry; eassumption. Qed.
Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_l _ R); [ | | solve [ eauto with nocore ] ] : typeclass_instances.
Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ eauto with nocore ] ] : typeclass_instances.

Axiom T : Type.
Axiom R : relation T.
Axiom R_trans : Transitive R. 
Axiom R_sym : Symmetric R.
Axiom a b c d : T.
Axiom F : T -> T -> T.
Axiom F_good : Proper (R ==> R ==> R) F.
Existing Instances R_trans R_sym F_good.

Goal R a b -> R c d -> R (F a c) (F b d).
Proof.
  intros H0 H1.
  rewrite H0.

cc @mattam82

Start by reading the Coq.Classes.Morphisms and Coq.Setoids.Setoid material referenced in the issue, then inspect how typeclass_instances handles Proper goals. Reproduce the supplied PER and setoid_rewrite example; done means the proposed PER_valid_l and PER_valid_r behavior works without breaking existing rewriting or typeclass resolution.