DEFINITION le_Sn_n()
TYPE =
       ∀n:nat.(not (le (S n) n))
BODY =
       assume n: nat
          we proceed by induction on n to prove not (le (S n) n)
             case O : ⇒
                the thesis becomes not (le (S O) O)
                   by (le_Sn_O .)
not (le (S O) O)
             case S : n0:nat ⇒
                the thesis becomes not (le (S (S n0)) (S n0))
                (IHn) by induction hypothesis we know not (le (S n0) n0)
                   we must prove not (le (S (S n0)) (S n0))
                   or equivalently (le (S (S n0)) (S n0))→False
                   suppose H: le (S (S n0)) (S n0)
                      by (le_S_n . . H)
                      we proved le (S n0) n0
                      by (IHn previous)
                      we proved False
                   we proved (le (S (S n0)) (S n0))→False
not (le (S (S n0)) (S n0))
          we proved not (le (S n) n)
       we proved ∀n:nat.(not (le (S n) n))