DEFINITION le_Sx_x()
TYPE =
       ∀x:nat.(le (S x) x)→∀P:Prop.P
BODY =
Show proof