DEFINITION le_not_lt()
TYPE =
       ∀n:nat.∀m:nat.(le n m)→(not (lt m n))
BODY =
        assume n: nat
        assume m: nat
        suppose H: le n m
          we proceed by induction on H to prove not (lt m n)
             case le_n : ⇒
                the thesis becomes not (lt n n)
                   by (lt_n_n .)
not (lt n n)
             case le_S : m0:nat :le n m0 ⇒
                the thesis becomes not (lt (S m0) n)
                (IHle) by induction hypothesis we know not (lt m0 n)
                   we must prove not (lt (S m0) n)
                   or equivalently (lt (S m0) n)→False
                   suppose H1: lt (S m0) n
                      consider H1
                      we proved lt (S m0) n
                      that is equivalent to le (S (S m0)) n
                      by (le_trans_S . . previous)
                      we proved le (S m0) n
                      that is equivalent to lt m0 n
                      by (IHle previous)
                      we proved False
                   we proved (lt (S m0) n)→False
not (lt (S m0) n)
          we proved not (lt m n)
       we proved ∀n:nat.∀m:nat.(le n m)→(not (lt m n))