DEFINITION le_x_pred_y()
TYPE =
       ∀y:nat.∀x:nat.(lt x y)→(le x (pred y))
BODY =
       assume y: nat
          we proceed by induction on y to prove ∀x:nat.(lt x y)→(le x (pred y))
             case O : ⇒
                the thesis becomes ∀x:nat.(lt x O)→(le x (pred O))
                    assume x: nat
                    suppose H: lt x O
                      (H0) 
                         by cases on H we prove (eq nat O O)→(le x O)
                            case le_n ⇒
                               the thesis becomes (eq nat (S x) O)→(le x O)
                               suppose H0: eq nat (S x) O
                                  (H1) 
                                     we proceed by induction on H0 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
                                        case refl_equal : ⇒
                                           the thesis becomes <λ:nat.Prop> CASE S x OF O⇒False | S ⇒True
                                              consider I
                                              we proved True
<λ:nat.Prop> CASE S x OF O⇒False | S ⇒True
<λ:nat.Prop> CASE O OF O⇒False | S ⇒True
                                  end of H1
                                  consider H1
                                  we proved <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
                                  that is equivalent to False
                                  we proceed by induction on the previous result to prove le x O
                                  we proved le x O
(eq nat (S x) O)→(le x O)
                            case le_S m:nat H0:le (S x) m ⇒
                               the thesis becomes ∀H1:(eq nat (S m) O).(le x O)
                               suppose H1: eq nat (S m) O
                                  (H2) 
                                     we proceed by induction on H1 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
                                        case refl_equal : ⇒
                                           the thesis becomes <λ:nat.Prop> CASE S m OF O⇒False | S ⇒True
                                              consider I
                                              we proved True
<λ:nat.Prop> CASE S m OF O⇒False | S ⇒True
<λ:nat.Prop> CASE O OF O⇒False | S ⇒True
                                  end of H2
                                  consider H2
                                  we proved <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
                                  that is equivalent to False
                                  we proceed by induction on the previous result to prove (le (S x) m)→(le x O)
                                  we proved (le (S x) m)→(le x O)
                                  by (previous H0)
                                  we proved le x O
∀H1:(eq nat (S m) O).(le x O)
(eq nat O O)→(le x O)
                      end of H0
                      by (refl_equal . .)
                      we proved eq nat O O
                      by (H0 previous)
                      we proved le x O
                      that is equivalent to le x (pred O)
∀x:nat.(lt x O)→(le x (pred O))
             case S : n:nat ⇒
                the thesis becomes ∀x:nat.∀H0:(lt x (S n)).(le x n)
                () by induction hypothesis we know ∀x:nat.(lt x n)→(le x (pred n))
                    assume x: nat
                    suppose H0: lt x (S n)
                      consider H0
                      we proved lt x (S n)
                      that is equivalent to le (S x) (S n)
                      by (le_S_n . . previous)
                      we proved le x n
                      that is equivalent to le x (pred (S n))
∀x:nat.∀H0:(lt x (S n)).(le x n)
          we proved ∀x:nat.(lt x y)→(le x (pred y))
       we proved ∀y:nat.∀x:nat.(lt x y)→(le x (pred y))