DEFINITION blt_lt()
TYPE =
       ∀x:nat.∀y:nat.(eq bool (blt y x) true)→(lt y x)
BODY =
       assume x: nat
          we proceed by induction on x to prove ∀y:nat.(eq bool (blt y x) true)→(lt y x)
             case O : ⇒
                the thesis becomes ∀y:nat.(eq bool (blt y O) true)→(lt y O)
                    assume y: nat
                    suppose H: eq bool (blt y O) true
                      (H0) 
                         by cases on H we prove (eq bool true true)→(lt y O)
                            case refl_equal ⇒
                               the thesis becomes (eq bool (blt y O) true)→(lt y O)
                               suppose H0: eq bool (blt y O) true
                                  (H1) 
                                     we proceed by induction on H0 to prove <λ:bool.Prop> CASE true OF true⇒False | false⇒True
                                        case refl_equal : ⇒
                                           the thesis becomes <λ:bool.Prop> CASE blt y O OF true⇒False | false⇒True
                                              consider I
                                              we proved True
<λ:bool.Prop> CASE blt y O OF true⇒False | false⇒True
<λ:bool.Prop> CASE true OF true⇒False | false⇒True
                                  end of H1
                                  consider H1
                                  we proved <λ:bool.Prop> CASE true OF true⇒False | false⇒True
                                  that is equivalent to False
                                  we proceed by induction on the previous result to prove lt y O
                                  we proved lt y O
(eq bool (blt y O) true)→(lt y O)
(eq bool true true)→(lt y O)
                      end of H0
                      by (refl_equal . .)
                      we proved eq bool true true
                      by (H0 previous)
                      we proved lt y O
∀y:nat.(eq bool (blt y O) true)→(lt y O)
             case S : n:nat ⇒
                the thesis becomes ∀y:nat.(eq bool (blt y (S n)) true)→(lt y (S n))
                (H) by induction hypothesis we know ∀y:nat.(eq bool (blt y n) true)→(lt y n)
                   assume y: nat
                      we proceed by induction on y to prove (eq bool (blt y (S n)) true)→(lt y (S n))
                         case O : ⇒
                            the thesis becomes (eq bool (blt O (S n)) true)→(lt O (S n))
                               we must prove (eq bool (blt O (S n)) true)→(lt O (S n))
                               or equivalently (eq bool true true)→(lt O (S n))
                               suppose : eq bool true true
                                  by (le_O_n .)
                                  we proved le O n
                                  by (le_n_S . . previous)
                                  we proved le (S O) (S n)
                                  by (le_n_S . . previous)
                                  we proved le (S (S O)) (S (S n))
                                  by (le_S_n . . previous)
                                  we proved le (S O) (S n)
                                  that is equivalent to lt O (S n)
                               we proved (eq bool true true)→(lt O (S n))
(eq bool (blt O (S n)) true)→(lt O (S n))
                         case S : n0:nat ⇒
                            the thesis becomes (eq bool (blt (S n0) (S n)) true)→(lt (S n0) (S n))
                            () by induction hypothesis we know 
                               eq bool <λn1:nat.bool> CASE n0 OF O⇒true | S m⇒blt m n true
                                 →lt n0 (S n)
                               we must prove (eq bool (blt (S n0) (S n)) true)→(lt (S n0) (S n))
                               or equivalently (eq bool (blt n0 n) true)→(lt (S n0) (S n))
                               suppose H1: eq bool (blt n0 n) true
                                  by (H . H1)
                                  we proved lt n0 n
                                  by (lt_n_S . . previous)
                                  we proved lt (S n0) (S n)
                               we proved (eq bool (blt n0 n) true)→(lt (S n0) (S n))
(eq bool (blt (S n0) (S n)) true)→(lt (S n0) (S n))
                      we proved (eq bool (blt y (S n)) true)→(lt y (S n))
∀y:nat.(eq bool (blt y (S n)) true)→(lt y (S n))
          we proved ∀y:nat.(eq bool (blt y x) true)→(lt y x)
       we proved ∀x:nat.∀y:nat.(eq bool (blt y x) true)→(lt y x)