DEFINITION le_Sn_O()
TYPE =
       ∀n:nat.(not (le (S n) O))
BODY =
       assume n: nat
          we must prove not (le (S n) O)
          or equivalently (le (S n) O)→False
          suppose H: le (S n) O
             we proceed by induction on H to prove IsSucc O
                case le_n : ⇒
                   the thesis becomes IsSucc (S n)
                      consider I
                      we proved True
IsSucc (S n)
                case le_S : m:nat :le (S n) m ⇒
                   the thesis becomes IsSucc (S m)
                   () by induction hypothesis we know IsSucc m
                      consider I
                      we proved True
IsSucc (S m)
             we proved IsSucc O
             that is equivalent to False
          we proved (le (S n) O)→False
          that is equivalent to not (le (S n) O)
       we proved ∀n:nat.(not (le (S n) O))