DEFINITION lt_neq()
TYPE =
       ∀x:nat.∀y:nat.(lt x y)→(not (eq nat x y))
BODY =
Show proof