DEFINITION lt_x_pred_y()
TYPE =
       ∀x:nat.∀y:nat.(lt x (pred y))→(lt (S x) y)
BODY =
        assume x: nat
        assume y: nat
          we proceed by induction on y to prove (lt x (pred y))→(lt (S x) y)
             case O : ⇒
                the thesis becomes (lt x (pred O))→(lt (S x) O)
                   we must prove (lt x (pred O))→(lt (S x) O)
                   or equivalently (lt x O)→(lt (S x) O)
                   suppose H: lt x O
                      by (lt_x_O . H .)
                      we proved lt (S x) O
                   we proved (lt x O)→(lt (S x) O)
(lt x (pred O))→(lt (S x) O)
             case S : n:nat ⇒
                the thesis becomes (lt x (pred (S n)))→(lt (S x) (S n))
                () by induction hypothesis we know (lt x (pred n))→(lt (S x) n)
                   we must prove (lt x (pred (S n)))→(lt (S x) (S n))
                   or equivalently (lt x n)→(lt (S x) (S n))
                   suppose H0: lt x n
                      consider H0
                      we proved lt x n
                      that is equivalent to le (S x) n
                      by (le_n_S . . previous)
                      we proved le (S (S x)) (S n)
                      by (le_n_S . . previous)
                      we proved le (S (S (S x))) (S (S n))
                      by (le_S_n . . previous)
                      we proved le (S (S x)) (S n)
                      that is equivalent to lt (S x) (S n)
                   we proved (lt x n)→(lt (S x) (S n))
(lt x (pred (S n)))→(lt (S x) (S n))
          we proved (lt x (pred y))→(lt (S x) y)
       we proved ∀x:nat.∀y:nat.(lt x (pred y))→(lt (S x) y)