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