DEFINITION le_or_lt()
TYPE =
       ∀n:nat.∀m:nat.(or (le n m) (lt m n))
BODY =
Show proof