DEFINITION lt_neq()
TYPE =
       ∀x:nat.∀y:nat.(lt x y)→(not (eq nat x y))
BODY =
        assume x: nat
        assume y: nat
        suppose H: lt x y
          we must prove not (eq nat x y)
          or equivalently (eq nat x y)→False
          suppose H0: eq nat x y
             (H1) 
                we proceed by induction on H0 to prove lt y y
                   case refl_equal : ⇒
                      the thesis becomes the hypothesis H
lt y y
             end of H1
             by (lt_n_n . H1)
             we proved False
          we proved (eq nat x y)→False
          that is equivalent to not (eq nat x y)
       we proved ∀x:nat.∀y:nat.(lt x y)→(not (eq nat x y))