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