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