DEFINITION lt_S_n()
TYPE =
       ∀n:nat.∀m:nat.(lt (S n) (S m))→(lt n m)
BODY =
        assume n: nat
        assume m: nat
        suppose H: lt (S n) (S m)
          consider H
          we proved lt (S n) (S m)
          that is equivalent to le (S (S n)) (S m)
          by (le_S_n . . previous)
          we proved le (S n) m
          that is equivalent to lt n m
       we proved ∀n:nat.∀m:nat.(lt (S n) (S m))→(lt n m)