(*s Definition of inequality *)

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