DEFINITION lt_gen_xS()
TYPE =
       ∀x:nat
         .∀n:nat
           .lt x (S n)
             →or (eq nat x O) (ex2 nat λm:nat.eq nat x (S m) λm:nat.lt m n)
BODY =
       assume x: nat
          we proceed by induction on x to prove 
             ∀n0:nat
               .lt x (S n0)
                 →or (eq nat x O) (ex2 nat λm:nat.eq nat x (S m) λm:nat.lt m n0)
             case O : ⇒
                the thesis becomes 
                ∀n:nat
                  .lt O (S n)
                    →or (eq nat O O) (ex2 nat λm:nat.eq nat O (S m) λm:nat.lt m n)
                    assume n: nat
                    suppose : lt O (S n)
                      by (refl_equal . .)
                      we proved eq nat O O
                      by (or_introl . . previous)
                      we proved or (eq nat O O) (ex2 nat λm:nat.eq nat O (S m) λm:nat.lt m n)

                      ∀n:nat
                        .lt O (S n)
                          →or (eq nat O O) (ex2 nat λm:nat.eq nat O (S m) λm:nat.lt m n)
             case S : n:nat ⇒
                the thesis becomes 
                ∀n0:nat
                  .∀H0:lt (S n) (S n0)
                    .or
                      eq nat (S n) O
                      ex2 nat λm:nat.eq nat (S n) (S m) λm:nat.lt m n0
                () by induction hypothesis we know 
                   ∀n0:nat
                     .lt n (S n0)
                       →or (eq nat n O) (ex2 nat λm:nat.eq nat n (S m) λm:nat.lt m n0)
                    assume n0: nat
                    suppose H0: lt (S n) (S n0)
                      (h1) 
                         by (refl_equal . .)
eq nat (S n) (S n)
                      end of h1
                      (h2) 
                         consider H0
                         we proved lt (S n) (S n0)
                         that is equivalent to le (S (S n)) (S n0)
                         by (le_S_n . . previous)
                         we proved le (S n) n0
lt n n0
                      end of h2
                      by (ex_intro2 . . . . h1 h2)
                      we proved ex2 nat λm:nat.eq nat (S n) (S m) λm:nat.lt m n0
                      by (or_intror . . previous)
                      we proved 
                         or
                           eq nat (S n) O
                           ex2 nat λm:nat.eq nat (S n) (S m) λm:nat.lt m n0

                      ∀n0:nat
                        .∀H0:lt (S n) (S n0)
                          .or
                            eq nat (S n) O
                            ex2 nat λm:nat.eq nat (S n) (S m) λm:nat.lt m n0
          we proved 
             ∀n0:nat
               .lt x (S n0)
                 →or (eq nat x O) (ex2 nat λm:nat.eq nat x (S m) λm:nat.lt m n0)
       we proved 
          ∀x:nat
            .∀n0:nat
              .lt x (S n0)
                →or (eq nat x O) (ex2 nat λm:nat.eq nat x (S m) λm:nat.lt m n0)