Cotransitivity

Stream: mathlib4

[Alex Meiburg]

Does Lean have a notion of cotransitivity? As used in e.g. Agda: https://agda.github.io/agda-stdlib/Relation.Binary.Definitions.html

Specifically, if R is transitive, then its negation fun x y => ¬(R x y) is cotransitive. This is distinct from intransitivity or antitransitivity. Important examples would be <, >, ≠, ≤, and ≥.

I ask because the function destutteris usually used with ≠, or if not, with other cotransitive properties. Lots of nice lemmas about it can be proven if you assume [Contransitive R] -- except that Cotransitive doesn't seem to exist. :)