theories/Num/NeqDef.v


1
2
3
4
5
6
7
8
9

(*s Definition of inequality *)

Require Params.
Require EqParams.
Definition neq [x,y:N] := (eqN x y)->False.

Infix 6 "<>" neq.