DEFINITION le_Sn_O()
TYPE =
       ∀n:nat.(not (le (S n) O))
BODY =
Show proof