DEFINITION not_eq_S()
TYPE =
       ∀n:nat.∀m:nat.(not (eq nat n m))→(not (eq nat (S n) (S m)))
BODY =
        assume n: nat
        assume m: nat
        suppose H: not (eq nat n m)
          we must prove not (eq nat (S n) (S m))
          or equivalently (eq nat (S n) (S m))→False
          suppose H0: eq nat (S n) (S m)
             by (eq_add_S . . H0)
             we proved eq nat n m
             by (H previous)
             we proved False
          we proved (eq nat (S n) (S m))→False
          that is equivalent to not (eq nat (S n) (S m))
       we proved ∀n:nat.∀m:nat.(not (eq nat n m))→(not (eq nat (S n) (S m)))