generalize RHS and LHS #1555

In Coq the predefined pattern for left and right pattern are associated with equality.

Notation RHS := (X in _ = X)%pattern.
Notation LHS := (X in X = _)%pattern.

would it be possible to have a more general version of RHS and LHS

Notation RHS := (_ X)%pattern.
Notation LHS := (_ X  _)%pattern.
Notation eqRHS := (X in _ = X)%pattern.
Notation eqLHS := (X in X = _)%pattern.

Pro : RHS and LHS will work with all infix symbol = _ == _ < <= .....

Cons : it is a breaking change. The current RHS find the first right hand-side of an equality. So rewrite -[LHS]mul1n on (1 = 2 -> False) works but our new version it will break and we will have to write rewrite -[eqLHS]mul1n instead .

I have tested on mathcomp out of the 400 occurrences of RHS (LHS) only a dozen actually broke.