NeqDef.v « Nat « Num « theories - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/theories/Num/Nat/NeqDef.v

blob: 8ce7df03a56572bb02b6223b02bd67af32818a58 (plain)


(*s Definition of inequality *)

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