Library Coqtail.mytheories.MyNeq

Require Setoid.

Add Parametric Relation (A : Type) : A (fun (x y : A) ⇒ x ≠ y)
symmetry proved by (@not_eq_sym A) as Neq.