DEFINITION le_gen_S()
TYPE =
       ∀m:nat
         .∀x:nat.(le (S m) x)→(ex2 nat λn:nat.eq nat x (S n) λn:nat.le m n)
BODY =
        assume m: nat
        assume x: nat
        suppose H: le (S m) x
          (H0) 
             by cases on H we prove (eq nat x x)→(ex2 nat λn0:nat.eq nat x (S n0) λn0:nat.le m n0)
                case le_n ⇒
                   the thesis becomes (eq nat (S m) x)→(ex2 nat λn0:nat.eq nat x (S n0) λn0:nat.le m n0)
                   suppose H0: eq nat (S m) x
                      we proceed by induction on H0 to prove ex2 nat λn0:nat.eq nat x (S n0) λn0:nat.le m n0
                         case refl_equal : ⇒
                            the thesis becomes ex2 nat λn:nat.eq nat (S m) (S n) λn:nat.le m n
                               (h1) 
                                  by (refl_equal . .)
eq nat (S m) (S m)
                               end of h1
                               (h2) by (le_n .) we proved le m m
                               by (ex_intro2 . . . . h1 h2)
ex2 nat λn:nat.eq nat (S m) (S n) λn:nat.le m n
                      we proved ex2 nat λn0:nat.eq nat x (S n0) λn0:nat.le m n0
(eq nat (S m) x)→(ex2 nat λn0:nat.eq nat x (S n0) λn0:nat.le m n0)
                case le_S m0:nat H0:le (S m) m0 ⇒
                   the thesis becomes ∀H1:(eq nat (S m0) x).(ex2 nat λn0:nat.eq nat x (S n0) λn0:nat.le m n0)
                   suppose H1: eq nat (S m0) x
                      suppose H2: le (S m) m0
                         (h1) 
                            by (refl_equal . .)
eq nat (S m0) (S m0)
                         end of h1
                         (h2) 
                            by (le_S . . H2)
                            we proved le (S m) (S m0)
                            by (le_S_n . . previous)
le m m0
                         end of h2
                         by (ex_intro2 . . . . h1 h2)
                         we proved ex2 nat λn:nat.eq nat (S m0) (S n) λn:nat.le m n
(le (S m) m0)→(ex2 nat λn:nat.eq nat (S m0) (S n) λn:nat.le m n)
                      by (previous H1 H0)
                      we proved ex2 nat λn0:nat.eq nat x (S n0) λn0:nat.le m n0
∀H1:(eq nat (S m0) x).(ex2 nat λn0:nat.eq nat x (S n0) λn0:nat.le m n0)
(eq nat x x)→(ex2 nat λn0:nat.eq nat x (S n0) λn0:nat.le m n0)
          end of H0
          by (refl_equal . .)
          we proved eq nat x x
          by (H0 previous)
          we proved ex2 nat λn0:nat.eq nat x (S n0) λn0:nat.le m n0
       we proved 
          ∀m:nat.∀x:nat.(le (S m) x)→(ex2 nat λn0:nat.eq nat x (S n0) λn0:nat.le m n0)