[Agda] (¬_ ∘ P) Respects

[Sergei Meshveliani]

(Suggestions and bug tracker on Standard library is on the Web.
But what is, please, the appropriate place to ask about  
Standard library features? to _discuss_ them?
)

People,
I need proofs for things like

  P Respects _≈_ → (¬_ ∘ P) Respects _≈_,
       
  x ≈ x' -> y ≈ y' -> x ∤ y -> x' ∤ y'   (for a generic "not divides").

And I write for this:

  ¬respects : ∀ {α α= β} →
              {A : Set α} → (_≈_ : Rel A α=) → Symmetric _≈_ →
              (P : A → Set β) → 
              P Respects _≈_ → (¬_ ∘ P) Respects _≈_
  ...
  ¬respects = ...


But has Standard library something for this?
If not, then needs it to have?

Thanks,

------
Sergei