DEFINITION le_antisym()
TYPE =
       ∀n:nat.∀m:nat.(le n m)→(le m n)→(eq nat n m)
BODY =
Show proof