DEFINITION lt_x_plus_x_Sy()
TYPE =
       ∀x:nat.∀y:nat.(lt x (plus x (S y)))
BODY =
        assume x: nat
        assume y: nat
          (h1) 
             by (le_plus_r . .)
             we proved le x (plus y x)
             by (le_n_S . . previous)
             we proved le (S x) (S (plus y x))
             by (le_n_S . . previous)
             we proved le (S (S x)) (S (S (plus y x)))
             by (le_S_n . . previous)
             we proved le (S x) (S (plus y x))
lt x (plus (S y) x)
          end of h1
          (h2) 
             by (plus_sym . .)
eq nat (plus x (S y)) (plus (S y) x)
          end of h2
          by (eq_ind_r . . . h1 . h2)
          we proved lt x (plus x (S y))
       we proved ∀x:nat.∀y:nat.(lt x (plus x (S y)))