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