DEFINITION le_lt_false()
TYPE =
       ∀x:nat.∀y:nat.(le x y)→(lt y x)→∀P:Prop.P
BODY =
        assume x: nat
        assume y: nat
        suppose H: le x y
        suppose H0: lt y x
        assume P: Prop
          by (le_not_lt . . H H0)
          we proved False
          we proceed by induction on the previous result to prove P
          we proved P
       we proved ∀x:nat.∀y:nat.(le x y)→(lt y x)→∀P:Prop.P