Add Hint Mode for Equivalence and friends

See also the discussion at #Rocq users > Trouble with two libraries interracting

Aside from Equivalence, modes are also added for related classes: Reflexive, Symmetric, Transitive, PreOrder. For the former, I removed an old "test".

Setting a mode for Reflexive relies on https://github.com/rocq-prover/rocq/pull/13969 (merged since 8.16 already).